theorem Th5: :: GEOMTRAP:5

for V being RealLinearSpace
for u, w being VECTOR of V ex y being VECTOR of V st u # y = w