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:2, FVSUM_1:3;
then A2:
( product the addF of F,n is commutative & product the addF of F,n is associative )
by Th14, Th15;
A3:
0. F is_a_unity_wrt the addF of F
by A1, Th3;
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:7;
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:3, SETWISEO:def 2;
then
product (comp F),
n is_an_inverseOp_wrt product the
addF of
F,
n
by A1, Lm1, Th17;
then A5:
x + y = the_unity_wrt (product the addF of F,n)
by FINSEQOP:def 1;
0. G is_a_unity_wrt the
addF of
G
by A1, Th3, Th16;
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, Th3, Th16;
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