let V be RealLinearSpace; :: thesis: for y, u, v, w being VECTOR of V st y + u = v + w holds
y - w = v - u
let y, u, v, w 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:10
.= (y + (u - u)) - w by RLVECT_1:28
.= ((v + w) + (- u)) - w by A1, RLVECT_1:def 6
.= (- u) + ((v + w) - w) by RLVECT_1:def 6
.= v - u by RLSUB_2:78 ; :: thesis: verum