let n be non empty Nat; :: thesis: for G being commutative Group
for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) holds
ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
let G be commutative Group; :: thesis: for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) holds
ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
let F be Group-like associative multMagma-Family of Seg n; :: thesis: ( ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) implies ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) )
set I = Seg n;
assume that
AS2: for i being Element of Seg n holds F . i is Subgroup of G and
AS3: for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) and
AS4: for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ; :: thesis: ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
LM1: for x being Element of (product F) holds
( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) )

proof

let x be Element of (product F); :: thesis: ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) )
W0: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
W12: dom (Carrier F) = Seg n by PARTFUN1:def 4;
dom x = Seg n by W0, PARTFUN1:def 4;
then reconsider s = x as FinSequence by FINSEQ_1:def 2;
W2: for i being Element of Seg n holds x . i in the carrier of (F . i)

proof

let i be Element of Seg n; :: thesis: x . i in the carrier of (F . i)
ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;
hence x . i in the carrier of (F . i) by W12, CARD_3:18, W0; :: thesis: verum

end;

for i being Nat st i in dom s holds
s . i in the carrier of G

proof

let i be Nat; :: thesis: ( i in dom s implies s . i in the carrier of G )
assume i in dom s ; :: thesis: s . i in the carrier of G
then reconsider j = i as Element of Seg n by W0, PARTFUN1:def 4;
W22: s . j in the carrier of (F . j) by W2;
F . j is Subgroup of G by AS2;
then the carrier of (F . j) c= the carrier of G by GROUP_2:def 5;
hence s . i in the carrier of G by W22; :: thesis: verum

end;

hence ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) ) by FINSEQ_2:14, CARD_3:18, W0, PARTFUN1:def 4; :: thesis: verum

end;

defpred S₁[ set , set ] means ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = $1 & $2 = Product s );
P1: for x being Element of (product F) ex y being Element of G st S₁[x,y]

proof

let x be Element of (product F); :: thesis: ex y being Element of G st S₁[x,y]
QR1: ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) ) by LM1;
reconsider s = x as FinSequence of G by LM1;
QR2: dom x = Seg n by LM1;
W2: for i being Element of Seg n holds x . i in the carrier of (F . i)

proof

let i be Element of Seg n; :: thesis: x . i in the carrier of (F . i)
ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;
hence x . i in the carrier of (F . i) by QR1; :: thesis: verum

end;

n in NAT by ORDINAL1:def 13;
then X1: len s = n by QR2, FINSEQ_1:def 3;

X2: now

let k be Element of Seg n; :: thesis: s . k in F . k
s . k in the carrier of (F . k) by W2;
hence s . k in F . k by STRUCT_0:def 5; :: thesis: verum

end;

take Product s ; :: thesis: S₁[x, Product s]
thus S₁[x, Product s] by X1, X2; :: thesis: verum

end;

consider f being Function of (product F),G such that
P2: for x being Element of the carrier of (product F) holds S₁[x,f . x] from FUNCT_2:sch 3(P1);
for a, b being Element of (product F) holds f . (a * b) = (f . a) * (f . b)

proof

let a, b be Element of (product F); :: thesis: f . (a * b) = (f . a) * (f . b)
QR1: ( a is FinSequence of G & dom a = Seg n & dom a = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
a . i in (Carrier F) . i ) ) by LM1;
reconsider a1 = a as FinSequence of G by LM1;
QR2: ( b is FinSequence of G & dom b = Seg n & dom b = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
b . i in (Carrier F) . i ) ) by LM1;
reconsider b1 = b as FinSequence of G by LM1;
QR3: ( a * b is FinSequence of G & dom (a * b) = Seg n & dom (a * b) = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
(a * b) . i in (Carrier F) . i ) ) by LM1;
reconsider ab1 = a * b as FinSequence of G by LM1;

K0: now

let k be Element of NAT ; :: thesis: ( k in dom ab1 implies ab1 . k = (a1 /. k) * (b1 /. k) )
assume k in dom ab1 ; :: thesis: ab1 . k = (a1 /. k) * (b1 /. k)
then reconsider k0 = k as Element of Seg n by LM1;
ex R being 1-sorted st
( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def 13;
then reconsider aa = a . k0 as Element of (F . k0) by QR1;
ex R being 1-sorted st
( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def 13;
then reconsider bb = b . k0 as Element of (F . k0) by QR2;
ex R being 1-sorted st
( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def 13;
then A1: aa = a1 /. k0 by PARTFUN1:def 8, QR1;
A2: bb = b1 /. k0 by PARTFUN1:def 8, QR2;
A3: F . k0 is Subgroup of G by AS2;
thus ab1 . k = aa * bb by GROUP_7:4
.= (a1 /. k) * (b1 /. k) by A1, A2, A3, GROUP_2:52 ; :: thesis: verum

end;

K1: ex sa being FinSequence of G st
( len sa = n & ( for k being Element of Seg n holds sa . k in F . k ) & sa = a & f . a = Product sa ) by P2;
K2: ex sb being FinSequence of G st
( len sb = n & ( for k being Element of Seg n holds sb . k in F . k ) & sb = b & f . b = Product sb ) by P2;
ex sab being FinSequence of G st
( len sab = n & ( for k being Element of Seg n holds sab . k in F . k ) & sab = a * b & f . (a * b) = Product sab ) by P2;
hence f . (a * b) = (f . a) * (f . b) by K0, K1, K2, GROUP_4:20; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (product F),G by GROUP_6:def 7;
take f ; :: thesis: ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )

now

let y be set ; :: thesis: ( y in the carrier of G implies y in rng f )
assume y in the carrier of G ; :: thesis: y in rng f
then consider s being FinSequence of G such that
R1: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & y = Product s ) by AS3;
W0: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
W11: dom s = Seg n by R1, FINSEQ_1:def 3;
W12: dom (Carrier F) = Seg n by PARTFUN1:def 4;
W2: for x being set st x in dom (Carrier F) holds
s . x in (Carrier F) . x

proof

let x be set ; :: thesis: ( x in dom (Carrier F) implies s . x in (Carrier F) . x )
assume x in dom (Carrier F) ; :: thesis: s . x in (Carrier F) . x
then reconsider i = x as Element of Seg n by PARTFUN1:def 4;
P2: s . i in F . i by R1;
ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;
hence s . x in (Carrier F) . x by STRUCT_0:def 5, P2; :: thesis: verum

end;

reconsider x = s as Element of (product F) by CARD_3:18, W0, W11, W12, W2;
ex t being FinSequence of G st
( len t = n & ( for k being Element of Seg n holds t . k in F . k ) & t = x & f . x = Product t ) by P2;
hence y in rng f by FUNCT_2:6, R1; :: thesis: verum

end;

then X1: the carrier of G c= rng f by TARSKI:def 3;
rng f = the carrier of G by X1, XBOOLE_0:def 10;
then P3: f is onto by FUNCT_2:def 3;
for x1, x2 being set st x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 implies x1 = x2 )
assume AS: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 ) ; :: thesis: x1 = x2
consider s being FinSequence of G such that
Q1: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x1 & f . x1 = Product s ) by P2, AS;
consider t being FinSequence of G such that
Q2: ( len t = n & ( for k being Element of Seg n holds t . k in F . k ) & t = x2 & f . x2 = Product t ) by P2, AS;
thus x1 = x2 by AS4, Q1, AS, Q2; :: thesis: verum

end;

then f is one-to-one by FUNCT_2:25;
hence ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) by P2, P3; :: thesis: verum