theorem Th8: :: ANALORT:8

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