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
proof
set B = the
addF of
F;
set C =
comp F;
let x be
Element of
G;
ALGSTR_0:def 16 x is right_complementable
reconsider y =
(product ((comp F),n)) . x as
Element of
G by FUNCT_2:5;
take
y
;
ALGSTR_0:def 11 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;
verum
end;
( 0. G = n |-> (0. F) & n |-> (0. F) is_a_unity_wrt product ( the addF of F,n) )
by A1, Th1, Th8;
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; verum