let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st v - u = y - w holds
u,v // w,y
let u, v, w, y be VECTOR of V; :: thesis: ( v - u = y - w implies u,v // w,y )
assume v - u = y - w ; :: thesis: u,v // w,y
then jj * (v - u) = jj * (y - w) ;
hence u,v // w,y ; :: thesis: verum