let GS be non empty addLoopStr ; :: thesis: ( the addF of GS is commutative & the addF of GS is associative & 0. GS is_a_unity_wrt the addF of GS & comp GS is_an_inverseOp_wrt the addF of GS implies GS is AbGroup )
assume that
A1: ( the addF of GS is commutative & the addF of GS is associative ) and
A2: 0. GS is_a_unity_wrt the addF of GS and
A3: comp GS is_an_inverseOp_wrt the addF of GS ; :: thesis: GS is AbGroup
A4: GS is right_complementable

proof

let x be Element of GS; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider b = (comp GS) . x as Element of GS ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: x + b = 0. GS
thus x + b = the_unity_wrt the addF of GS by A3
.= 0. GS by A2, BINOP_1:def 8 ; :: thesis: verum

end;

for x, y, z being Element of GS holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. GS) = x ) by A1, A2, BINOP_1:3;
hence GS is AbGroup by A4, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum