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. G = n .--> (0. F)
;
A4:
0. F is_a_unity_wrt the addF of F
by A1, Th3;
A5:
n .--> (0. F) is_a_unity_wrt product the addF of F,n
by A1, Th3, Th16;
G is right_complementable
proof
let x be
Element of
G;
:: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
set C =
comp F;
set B = the
addF of
F;
A6:
( the
addF of
F is
associative &
comp F is_an_inverseOp_wrt the
addF of
F )
by A1, Lm1, FVSUM_1:3;
the
addF of
F is
having_a_unity
by A4, SETWISEO:def 2;
then A7:
product (comp F),
n is_an_inverseOp_wrt product the
addF of
F,
n
by A6, Th17;
reconsider y =
(product (comp F),n) . x as
Element of
G by FUNCT_2:7;
take
y
;
:: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G
A8:
0. G is_a_unity_wrt the
addF of
G
by A1, Th3, Th16;
x + y = the_unity_wrt (product the addF of F,n)
by A7, FINSEQOP:def 1;
hence
x + y = 0. G
by A8, BINOP_1:def 8;
:: thesis: verum
end;
hence
addLoopStr(# (n -tuples_on the carrier of F),(product the addF of F,n),(n .--> (0. F)) #) is strict AbGroup
by A2, A3, A5, Lm2, Lm3; :: thesis: verum