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 and
A2: the addF of GS is associative and
A3: 0. GS is_a_unity_wrt the addF of GS and
A4: comp GS is_an_inverseOp_wrt the addF of GS ; :: thesis: GS is AbGroup
A5: 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, A3, BINOP_1:11, BINOP_1:def 2, BINOP_1:def 3;
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 A4, FINSEQOP:def 1
.= 0. GS by A3, BINOP_1:def 8 ; :: thesis: verum

end;

hence GS is AbGroup by A5, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7; :: thesis: verum