for V being RealLinearSpace
for w, y, u, v being VECTOR of V
for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )