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

( 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

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

for x, y, z being Element of GS holds
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;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

( 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