let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st y + u = v + w holds
y - w = v - u
let u, v, w, y be VECTOR of V; :: thesis: ( y + u = v + w implies y - w = v - u )
assume A1: y + u = v + w ; :: thesis: y - w = v - u
thus y - w = (y + (0. V)) - w by RLVECT_1:4
.= (y + (u - u)) - w by RLVECT_1:15
.= ((v + w) + (- u)) - w by A1, RLVECT_1:def 3
.= (- u) + ((v + w) - w) by RLVECT_1:def 3
.= v - u by RLSUB_2:61 ; :: thesis: verum