deffunc H₂( 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 = H₂(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 ; :: according to RLVECT_1:def 6 :: thesis: (A + B) + C = A + (B + C)
reconsider A' = A, B' = B, C' = C as Chain of k,G ;
thus (A + B) + C = op . (A' + B'),C by A1
.= (A' + B') + C' by A1
.= A' + (B' + C') by XBOOLE_1:91
.= op . A,(B' + C') 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 ; :: according to RLVECT_1:def 7 :: thesis: A + (0. addLoopStr(# (bool (cells k,G)),op,(0_ k,G) #)) = A
reconsider A' = A as Chain of k,G ;
thus A + (0. addLoopStr(# (bool (cells k,G)),op,(0_ k,G) #)) = A' + (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 ; :: according to ALGSTR_0:def 16 :: thesis: A is right_complementable
reconsider A' = 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 = A' + A' 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 ; :: according to RLVECT_1:def 5 :: thesis: A + B = B + A
reconsider A' = A, B' = B as Chain of k,G ;
thus A + B = A' + B' 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
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) )
thus the carrier of ch = bool (cells k,G) ; :: thesis: ( 0. ch = 0_ k,G & ( for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) )
thus 0. ch = 0_ k,G ; :: thesis: for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B'
let A, B be Element of ; :: thesis: for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B'
let A', B' be Chain of k,G; :: thesis: ( A = A' & B = B' implies A + B = A' + B' )
assume that
A5: A = A' and
A6: B = B' ; :: thesis: A + B = A' + B'
thus A + B = A' + B' by A1, A5, A6; :: thesis: verum