set G = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);

reconsider G = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) as non empty addLoopStr ;

( the addF of F is commutative & the addF of F is associative ) by A1, FVSUM_1:1, FVSUM_1:2;

then A2: ( product ( the addF of F,n) is commutative & product ( the addF of F,n) is associative ) by Th6, Th7;

A3: 0. F is_a_unity_wrt the addF of F by A1, Th1;

A4: G is right_complementable

hence addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup by A2, A4, Lm2, Lm3; :: thesis: verum

reconsider G = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) as non empty addLoopStr ;

( the addF of F is commutative & the addF of F is associative ) by A1, FVSUM_1:1, FVSUM_1:2;

then A2: ( product ( the addF of F,n) is commutative & product ( the addF of F,n) is associative ) by Th6, Th7;

A3: 0. F is_a_unity_wrt the addF of F by A1, Th1;

A4: G is right_complementable

proof

( 0. G = n |-> (0. F) & n |-> (0. F) is_a_unity_wrt product ( the addF of F,n) )
by A1, Th1, Th8;
set B = the addF of F;

set C = comp F;

let x be Element of G; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider y = (product ((comp F),n)) . x as Element of G by FUNCT_2:5;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G

( the addF of F is associative & the addF of F is having_a_unity ) by A1, A3, FVSUM_1:2, SETWISEO:def 2;

then product ((comp F),n) is_an_inverseOp_wrt product ( the addF of F,n) by A1, Lm1, Th9;

then A5: x + y = the_unity_wrt (product ( the addF of F,n)) ;

0. G is_a_unity_wrt the addF of G by A1, Th1, Th8;

hence x + y = 0. G by A5, BINOP_1:def 8; :: thesis: verum

end;set C = comp F;

let x be Element of G; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider y = (product ((comp F),n)) . x as Element of G by FUNCT_2:5;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G

( the addF of F is associative & the addF of F is having_a_unity ) by A1, A3, FVSUM_1:2, SETWISEO:def 2;

then product ((comp F),n) is_an_inverseOp_wrt product ( the addF of F,n) by A1, Lm1, Th9;

then A5: x + y = the_unity_wrt (product ( the addF of F,n)) ;

0. G is_a_unity_wrt the addF of G by A1, Th1, Th8;

hence x + y = 0. G by A5, BINOP_1:def 8; :: thesis: verum

hence addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup by A2, A4, Lm2, Lm3; :: thesis: verum