let n be non zero Nat; :: thesis:
let G be commutative Group; :: thesis:
let F be Group-like associative multMagma-Family of Seg n; :: thesis:
set I = Seg n;
assume that
A1: for i being Element of Seg n holds F . i is Subgroup of G and
A2: 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
A3: 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:
A4: 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 ) )

end;

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

let i be Nat; :: thesis:
assume i in dom s ; :: thesis:
then reconsider j = i as Element of Seg n by A5, PARTFUN1:def 2;
A8: s . j in the carrier of (F . j) by A7;
F . j is Subgroup of G by A1;
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 A8; :: thesis:

end;

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 );
A9: for x being Element of (product F) ex y being Element of G st S₁[x,y]

let x be Element of (product F); :: thesis:
A10: ( 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 A4;
reconsider s = x as FinSequence of G by A4;
A11: dom x = Seg n by A4;
A12: for i being Element of Seg n holds x . i in the carrier of (F . i)

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

end;

end;

end;

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

let a, b be Element of (product F); :: thesis:
A16: ( 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 A4;
reconsider a1 = a as FinSequence of G by A4;
A17: ( 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 A4;
reconsider b1 = b as FinSequence of G by A4;
reconsider ab1 = a * b as FinSequence of G by A4;

let k be Nat; :: thesis:
assume k in dom ab1 ; :: thesis:
then reconsider k0 = k as Element of Seg n by A4;
ex R being 1-sorted st
( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def 15;
then reconsider aa = a . k0 as Element of (F . k0) by A16;
ex R being 1-sorted st
( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def 15;
then reconsider bb = b . k0 as Element of (F . k0) by A17;
A19: aa = a1 /. k0 by A16, PARTFUN1:def 6;
A20: bb = b1 /. k0 by A17, PARTFUN1:def 6;
A21: F . k0 is Subgroup of G by A1;
thus ab1 . k = aa * bb by GROUP_7:1
.= (a1 /. k) * (b1 /. k) by A19, A20, A21, GROUP_2:43 ; :: thesis:

end;

A22: 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 A15;
A23: 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 A15;
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 A15;
hence f . (a * b) = (f . a) * (f . b) by A18, A22, A23, GROUP_4:17; :: thesis:

end;

then reconsider f = f as Homomorphism of (product F),G by GROUP_6:def 6;
take f ; :: thesis:

let x be object ; :: thesis:
assume x in dom (Carrier F) ; :: thesis:
then reconsider i = x as Element of Seg n ;
A29: s . i in F . i by A24;
ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;
hence s . x in (Carrier F) . x by A29, STRUCT_0:def 5; :: thesis:

end;

reconsider x = s as Element of (product F) by A25, A26, A27, A28, CARD_3:9;
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 A15;
hence y in rng f by A24, FUNCT_2:4; :: thesis:

end;

let x1, x2 be object ; :: thesis:
assume A32: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 ) ; :: thesis:
consider s being FinSequence of G such that
A33: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x1 & f . x1 = Product s ) by A15, A32;
consider t being FinSequence of G such that
A34: ( len t = n & ( for k being Element of Seg n holds t . k in F . k ) & t = x2 & f . x2 = Product t ) by A15, A32;
thus x1 = x2 by A3, A33, A32, A34; :: thesis:

end;

then f is one-to-one by FUNCT_2:19;
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 A15, A31; :: thesis: