let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, w being Element of V holds
( v + w = 0. V iff - v = w )
let v, w be Element of V; :: thesis: ( v + w = 0. V iff - v = w )
( v + w = 0. V implies - v = w )

proof

assume A1: v + w = 0. V ; :: thesis: - v = w
thus w = (0. V) + w by RLVECT_1:4
.= ((- v) + v) + w by RLVECT_1:5
.= (- v) + (0. V) by A1, RLVECT_1:def 3
.= - v by RLVECT_1:4 ; :: thesis: verum

end;

hence ( v + w = 0. V iff - v = w ) by RLVECT_1:5; :: thesis: verum