Define inner product spaces

[lowasser]

The only hard part, I think, will be establishing an appropriate version of the condition of positive definiteness.

I think the appropriate version is a rule that the inner product of x and x is always nonnegative, and then extensionality of the induced metric: if the inner product of x and x is zero, then x is zero.

[lowasser]

I suppose normed spaces should come first...

[lowasser]

As pointed out elsewhere, Theorem 4, the Pythagorean Theorem, falls out of the definition of inner product spaces almost immediately.