let R be Ring; :: thesis: for V being RightMod of R
for v, v1, v2 being Vector of V holds
( v = v1 + v2 iff v1 = v - v2 )
let V be RightMod of R; :: thesis: for v, v1, v2 being Vector of V holds
( v = v1 + v2 iff v1 = v - v2 )
let v, v1, v2 be Vector of V; :: thesis: ( v = v1 + v2 iff v1 = v - v2 )
thus ( v = v1 + v2 implies v1 = v - v2 ) :: thesis: ( v1 = v - v2 implies v = v1 + v2 )

proof

assume A1: v = v1 + v2 ; :: thesis: v1 = v - v2
thus v1 = (0. V) + v1 by RLVECT_1:def 4
.= (v + (- (v2 + v1))) + v1 by A1, VECTSP_1:19
.= (v + ((- v2) + (- v1))) + v1 by RLVECT_1:31
.= ((v + (- v2)) + (- v1)) + v1 by RLVECT_1:def 3
.= (v + (- v2)) + ((- v1) + v1) by RLVECT_1:def 3
.= (v + (- v2)) + (0. V) by RLVECT_1:5
.= v - v2 by RLVECT_1:def 4 ; :: thesis: verum

end;

assume A2: v1 = v - v2 ; :: thesis: v = v1 + v2
thus v = v + (0. V) by RLVECT_1:def 4
.= v + (v1 + (- v1)) by RLVECT_1:5
.= (v + v1) + (- (v - v2)) by A2, RLVECT_1:def 3
.= (v + v1) + ((- v) + v2) by RLVECT_1:33
.= ((v + v1) + (- v)) + v2 by RLVECT_1:def 3
.= ((v + (- v)) + v1) + v2 by RLVECT_1:def 3
.= ((0. V) + v1) + v2 by RLVECT_1:5
.= v1 + v2 by RLVECT_1:def 4 ; :: thesis: verum