deffunc H_{2}( 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_{2}(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

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

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

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

A3:
addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) is right_zeroed
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;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

proof

A4:
addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) is right_complementable
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;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

proof

addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) is Abelian
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;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

proof

then reconsider ch = addLoopStr(# (bool (cells (k,G))),op,(0_ (k,G)) #) as strict AbGroup by A2, A3, A4;
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;reconsider A9 = A, B9 = B as Chain of k,G ;

thus A + B = A9 + B9 by A1

.= B + A by A1 ; :: thesis: verum

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