theorem :: ANALMETR:33

for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfSp