let IT be Element of V; :: thesis: ( IT = - v iff v + IT = 0. V )
consider v1 being Element of V such that
A2: v + v1 = 0. V by A1, ALGSTR_0:def 11;
A3: V is right_add-cancelable by A1, Th3;
A4: 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, A2
.= (0. V) + v1 by A1 ;
hence v1 + v = 0. V by A3, ALGSTR_0:def 4; :: thesis: verum
end;
(v + (- v)) + v = v + ((- v) + v) by A1
.= v + (0. V) by A3, A4, ALGSTR_0:def 13
.= (0. V) + v by A1 ;
hence ( IT = - v implies v + IT = 0. V ) by A3, ALGSTR_0:def 4; :: thesis: ( v + IT = 0. V implies IT = - v )
assume A5: v + IT = 0. V ; :: thesis: IT = - v
thus IT = (0. V) + IT by A1
.= ((- v) + v) + IT by A3, A4, ALGSTR_0:def 13
.= (- v) + (0. V) by A1, A5
.= - v by A1 ; :: thesis: verum