let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, v1, v2 being Element of V holds
( v = v1 + v2 iff v1 = v - v2 )
let v, v1, v2 be Element 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 v = v1 + v2 ; :: thesis: v1 = v - v2
hence v - v2 = v1 + (v2 - v2) by RLVECT_1:def 3
.= v1 + (0. V) by VECTSP_1:19
.= v1 ;
:: thesis: verum

end;

thus ( v1 = v - v2 implies v = v1 + v2 ) :: thesis: verum

proof

assume v1 = v - v2 ; :: thesis: v = v1 + v2
hence v1 + v2 = v + ((- v2) + v2) by RLVECT_1:def 3
.= v + (0. V) by RLVECT_1:5
.= v ;
:: thesis: verum

end;