let V be RealLinearSpace; :: thesis: for v, u, y, w being VECTOR of V st v - u = y - w holds
u,v // w,y
let v, u, y, w 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 1 * (v - u) = 1 * (y - w) ;
hence u,v // w,y by Def1; :: thesis: verum