for V being RealLinearSpace
for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )