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 )

( 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

hence
( v + w = 0. V iff - v = w )
by RLVECT_1:5; :: thesis: verum
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;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