let n be non zero 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 (),G st
( f is bijective & ( for x being Element of () 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 (),G st
( f is bijective & ( for x being Element of () 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 (),G st
( f is bijective & ( for x being Element of () 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
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: ex f being Homomorphism of (),G st
( f is bijective & ( for x being Element of () 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 ) ) )

A4: for x being Element of () holds
( x is FinSequence of G & dom x = Seg n & dom x = dom () & ( for i being set st i in dom () holds
x . i in () . i ) )
proof
let x be Element of (); :: thesis: ( x is FinSequence of G & dom x = Seg n & dom x = dom () & ( for i being set st i in dom () holds
x . i in () . i ) )

A5: the carrier of () = product () by GROUP_7:def 2;
A6: dom () = Seg n by PARTFUN1:def 2;
dom x = Seg n by ;
then reconsider s = x as FinSequence by FINSEQ_1:def 2;
A7: 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 & () . i = the carrier of R ) by PRALG_1:def 13;
hence x . i in the carrier of (F . i) by ; :: 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 ;
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: verum
end;
hence ( x is FinSequence of G & dom x = Seg n & dom x = dom () & ( for i being set st i in dom () holds
x . i in () . i ) ) by ; :: thesis: verum
end;
defpred S1[ 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 () ex y being Element of G st S1[x,y]
proof
let x be Element of (); :: thesis: ex y being Element of G st S1[x,y]
A10: ( x is FinSequence of G & dom x = Seg n & dom x = dom () & ( for i being set st i in dom () holds
x . i in () . 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)
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 & () . i = the carrier of R ) by PRALG_1:def 13;
hence x . i in the carrier of (F . i) by A10; :: thesis: verum
end;
n in NAT by ORDINAL1:def 12;
then A13: len s = n by ;
A14: now :: thesis: for k being Element of Seg n holds s . k in F . k
let k be Element of Seg n; :: thesis: s . k in F . k
s . k in the carrier of (F . k) by A12;
hence s . k in F . k by STRUCT_0:def 5; :: thesis: verum
end;
take Product s ; :: thesis: S1[x, Product s]
thus S1[x, Product s] by ; :: thesis: verum
end;
consider f being Function of (),G such that
A15: for x being Element of the carrier of () holds S1[x,f . x] from for a, b being Element of () holds f . (a * b) = (f . a) * (f . b)
proof
let a, b be Element of (); :: thesis: f . (a * b) = (f . a) * (f . b)
A16: ( a is FinSequence of G & dom a = Seg n & dom a = dom () & ( for i being set st i in dom () holds
a . i in () . 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 () & ( for i being set st i in dom () holds
b . i in () . i ) ) by A4;
reconsider b1 = b as FinSequence of G by A4;
reconsider ab1 = a * b as FinSequence of G by A4;
A18: now :: thesis: for k being Nat st k in dom ab1 holds
ab1 . k = (a1 /. k) * (b1 /. k)
let k be 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 A4;
ex R being 1-sorted st
( R = F . k0 & () . k0 = the carrier of R ) by PRALG_1:def 13;
then reconsider aa = a . k0 as Element of (F . k0) by A16;
ex R being 1-sorted st
( R = F . k0 & () . k0 = the carrier of R ) by PRALG_1:def 13;
then reconsider bb = b . k0 as Element of (F . k0) by A17;
A19: aa = a1 /. k0 by ;
A20: bb = b1 /. k0 by ;
A21: F . k0 is Subgroup of G by A1;
thus ab1 . k = aa * bb by GROUP_7:1
.= (a1 /. k) * (b1 /. k) by ; :: thesis: verum
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 ; :: thesis: verum
end;
then reconsider f = f as Homomorphism of (),G by GROUP_6:def 6;
take f ; :: thesis: ( f is bijective & ( for x being Element of () 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 :: thesis: for y being object st y in the carrier of G holds
y in rng f
let y be object ; :: 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
A24: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & y = Product s ) by A2;
A25: the carrier of () = product () by GROUP_7:def 2;
A26: dom s = Seg n by ;
A27: dom () = Seg n by PARTFUN1:def 2;
A28: for x being object st x in dom () holds
s . x in () . x
proof
let x be object ; :: thesis: ( x in dom () implies s . x in () . x )
assume x in dom () ; :: thesis: s . x in () . x
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 & () . i = the carrier of R ) by PRALG_1:def 13;
hence s . x in () . x by ; :: thesis: verum
end;
reconsider x = s as Element of () by ;
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 ; :: thesis: verum
end;
then A30: the carrier of G c= rng f by TARSKI:def 3;
rng f = the carrier of G by ;
then A31: f is onto by FUNCT_2:def 3;
for x1, x2 being object st x1 in the carrier of () & x2 in the carrier of () & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in the carrier of () & x2 in the carrier of () & f . x1 = f . x2 implies x1 = x2 )
assume A32: ( x1 in the carrier of () & x2 in the carrier of () & f . x1 = f . x2 ) ; :: thesis: x1 = x2
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 ;
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 ;
thus x1 = x2 by A3, A33, A32, A34; :: thesis: verum
end;
then f is one-to-one by FUNCT_2:19;
hence ( f is bijective & ( for x being Element of () 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 ; :: thesis: verum