for V being RealLinearSpace
for u, v, w being VECTOR of V holds
( u,v // w,w & u,u // v,w ) ;