theorem Th6: :: ANALORT:6

for V being RealLinearSpace
for u, v, x, y being VECTOR of V st Gen x,y & Ortm (x,y,u) = Ortm (x,y,v) holds
u = v