theorem Th13: :: ANALORT:13

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