let V be RealLinearSpace; :: thesis: for v, w being VECTOR of V holds
( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
let v, w be VECTOR of V; :: thesis: ( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus (v + w) - v = w by RLSUB_2:61; :: thesis: ( (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus (w + v) - v = w by RLSUB_2:61; :: thesis: ( (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus A1: (v - v) + w = (0. V) + w by RLVECT_1:15
.= w by RLVECT_1:4 ; :: thesis: ( (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus (w - v) + v = w by RLSUB_2:61; :: thesis: ( v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus ( v + (w - v) = w & w + (v - v) = w & v - (v - w) = w ) by A1, RLSUB_2:61, RLVECT_1:29; :: thesis: verum