let IT be Element of V; :: thesis: ( IT = - v iff v + IT = 0. V )
consider v1 being Element of V such that
A3: v + v1 = 0. V by A2, ALGSTR_0:def 11;
A4: V is right_add-cancelable by A1, Th9;
then A5: v is right_add-cancelable ;
A6: v1 is right_add-cancelable by A4;
A7: v is left_complementable

proof

take v1 ; :: according to ALGSTR_0:def 10 :: thesis: v1 + v = 0. V
(v1 + v) + v1 = v1 + (0. V) by A1, A3, Def6
.= v1 by A1, Th10
.= (0. V) + v1 by A1, Th10 ;
hence v1 + v = 0. V by A6, ALGSTR_0:def 4; :: thesis: verum

end;

(v + (- v)) + v = v + ((- v) + v) by A1, Def6
.= v + (0. V) by A5, A7, ALGSTR_0:def 13
.= v by A1, Th10
.= (0. V) + v by A1, Th10 ;
hence ( IT = - v implies v + IT = 0. V ) by A5, ALGSTR_0:def 4; :: thesis: ( v + IT = 0. V implies IT = - v )
assume A8: v + IT = 0. V ; :: thesis: IT = - v
thus IT = (0. V) + IT by A1, Th10
.= ((- v) + v) + IT by A5, A7, ALGSTR_0:def 13
.= (- v) + (0. V) by A1, A8, Def6
.= - v by A1, Th10 ; :: thesis: verum