deffunc H2( Chain of k,G, Chain of k,G) -> Chain of k,G = $1 + $2;
consider op being BinOp of (bool (cells (k,G))) such that
A1: for A, B being Chain of k,G holds op . (A,B) = H2(A,B) from BINOP_1:sch 4();
 set ch = addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #);
A2: addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) is add-associative
proof
let A, B, C be Element of addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #); :: according to RLVECT_1:def 3 :: thesis: (A + B) + C = A + (B + C)
reconsider A9 = A, B9 = B, C9 = C as Chain of k,G ;
thus (A + B) + C = op . ((A9 + B9),C) by A1
.= (A9 + B9) + C9 by A1
.= A9 + (B9 + C9) by XBOOLE_1:91
.= op . (A,(B9 + C9)) by A1
.= A + (B + C) by A1 ; :: thesis: verum
end;
A3: addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) is right_zeroed
proof
let A be Element of addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #); :: according to RLVECT_1:def 4 :: thesis: A + (0. addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #)) = A
reconsider A9 = A as Chain of k,G ;
thus A + (0. addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #)) = A9 + (0_ (k,G)) by A1
.= A ; :: thesis: verum
end;
A4: addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) is right_complementable
proof
let A be Element of addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #); :: according to ALGSTR_0:def 16 :: thesis: A is right_complementable
reconsider A9 = A as Chain of k,G ;
take A ; :: according to ALGSTR_0:def 11 :: thesis: A + A = 0. addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #)
thus A + A = A9 + A9 by A1
.= 0. addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) by XBOOLE_1:92 ; :: thesis: verum
end;
addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) is Abelian
proof
let A, B be Element of addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #); :: according to RLVECT_1:def 2 :: thesis: A + B = B + A
reconsider A9 = A, B9 = B as Chain of k,G ;
thus A + B = A9 + B9 by A1
.= B + A by A1 ; :: thesis: verum
end;
then reconsider ch = addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) as strict AbGroup by A2, A3, A4;
take ch ; :: thesis: ( the carrier of ch = bool (cells (k,G)) & 0. ch = 0_ (k,G) & ( for A, B being Element of ch
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) )
thus the carrier of ch = bool (cells (k,G)) ; :: thesis: ( 0. ch = 0_ (k,G) & ( for A, B being Element of ch
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) )
thus 0. ch = 0_ (k,G) ; :: thesis: for A, B being Element of ch
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9
let A, B be Element of ch; :: thesis: for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9
let A9, B9 be Chain of k,G; :: thesis: ( A = A9 & B = B9 implies A + B = A9 + B9 )
assume that
A5: A = A9 and
A6: B = B9 ; :: thesis: A + B = A9 + B9
thus A + B = A9 + B9 by A1, A5, A6; :: thesis: verum