for V being RealLinearSpace
for u, x, y being VECTOR of V
for n being Real st Gen x,y holds
Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))