let B be non empty set ; :: thesis: for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm & P = om1 ! A,nd holds
addLoopStr(# B,P,e #) is AbGroup
let P be BinOp of B; :: thesis: for e being Element of B st B = A \ {nd} & e = nm & P = om1 ! A,nd holds
addLoopStr(# B,P,e #) is AbGroup
let e be Element of B; :: thesis: ( B = A \ {nd} & e = nm & P = om1 ! A,nd implies addLoopStr(# B,P,e #) is AbGroup )
assume A1: ( B = A \ {nd} & e = nm & P = om1 ! A,nd ) ; :: thesis: addLoopStr(# B,P,e #) is AbGroup
A2: for a, b, c being Element of B holds P . (P . a,b),c = P . a,(P . b,c)

proof

let a, b, c be Element of B; :: thesis: P . (P . a,b),c = P . a,(P . b,c)
( a = In 1,2 & b = In 1,2 & c = In 1,2 ) by A1, Lm17, TARSKI:def 1;
hence P . (P . a,b),c = P . a,(P . b,c) by A1, Lm17, TARSKI:def 1; :: thesis: verum

end;

A3: for a being Element of addLoopStr(# B,P,e #) holds a + (0. addLoopStr(# B,P,e #)) = a

proof

let a be Element of addLoopStr(# B,P,e #); :: thesis: a + (0. addLoopStr(# B,P,e #)) = a
a = In 1,2 by A1, Lm17, TARSKI:def 1;
hence a + (0. addLoopStr(# B,P,e #)) = a by A1, Lm17, TARSKI:def 1; :: thesis: verum

end;

A4: addLoopStr(# B,P,e #) is right_complementable

proof

let a be Element of addLoopStr(# B,P,e #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
take a ; :: according to ALGSTR_0:def 11 :: thesis: a + a = 0. addLoopStr(# B,P,e #)
thus a + a = 0. addLoopStr(# B,P,e #) by A1, Lm17, TARSKI:def 1; :: thesis: verum

end;

A5: for a, b, c being Element of addLoopStr(# B,P,e #) holds (a + b) + c = a + (b + c) by A2;
for a, b being Element of addLoopStr(# B,P,e #) holds a + b = b + a

proof

let a, b be Element of addLoopStr(# B,P,e #); :: thesis: a + b = b + a
( a = In 1,2 & b = In 1,2 ) by A1, Lm17, TARSKI:def 1;
hence a + b = b + a ; :: thesis: verum

end;

hence addLoopStr(# B,P,e #) is AbGroup by A3, A4, A5, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7; :: thesis: verum