let V be RealLinearSpace; :: thesis: for y, v, w, u being VECTOR of V st y = (v + w) - u holds
( u,v // w,y & u,w // v,y )
let y, v, w, u be VECTOR of V; :: thesis: ( y = (v + w) - u implies ( u,v // w,y & u,w // v,y ) )
set y = (v + w) - u;
( ((v + w) - u) + u = v + w & ((v + w) - u) + u = w + v ) by RLSUB_2:78;
then ( ((v + w) - u) - v = w - u & ((v + w) - u) - w = v - u ) by Th9;
hence ( y = (v + w) - u implies ( u,v // w,y & u,w // v,y ) ) by Th24; :: thesis: verum