let B be non empty set ; 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; 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; ( B = A \ {nd} & e = nm implies addLoopStr(# B,P,e #) is AbGroup )
assume that
A1:
B = A \ {nd}
and
A2:
e = nm
; addLoopStr(# B,P,e #) is AbGroup
A3:
addLoopStr(# B,P,e #) is right_complementable
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;
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;
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
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 #);
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;
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; verum