theorem Th30: :: ANALMETR:30

for V being RealLinearSpace
for w, y being VECTOR of V
for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds
p = q