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 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 holds
addLoopStr(# B,P,e #) is AbGroup
let e be Element of B; :: thesis: ( B = A \ {nd} & e = nm implies addLoopStr(# B,P,e #) is AbGroup )
assume that
A1: B = A \ {nd} and
A2: e = nm ; :: thesis: addLoopStr(# B,P,e #) is AbGroup
A3: 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, A2, Lm19, TARSKI:def 1; :: thesis: verum
end;
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)))
A4: b = In (1,2) by A1, Lm19, TARSKI:def 1;
A5: c = In (1,2) by A1, Lm19, TARSKI:def 1;
a = In (1,2) by A1, Lm19, TARSKI:def 1;
hence P . ((P . (a,b)),c) = P . (a,(P . (b,c))) by A1, A4, A5, Lm19, TARSKI:def 1; :: thesis: verum
end;
then A6: for a, b, c being Element of addLoopStr(# B,P,e #) holds (a + b) + c = a + (b + c) ;
A7: 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) by A1, Lm19, TARSKI:def 1;
hence a + b = b + a by A1, Lm19, TARSKI:def 1; :: thesis: verum
end;
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, Lm19, TARSKI:def 1;
hence a + (0. addLoopStr(# B,P,e #)) = a by A1, Lm19, TARSKI:def 1; :: thesis: verum
end;
hence addLoopStr(# B,P,e #) is AbGroup by A3, A6, A7, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum