theorem Th15: :: ANALORT:15

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