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 (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
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 (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 ) ) )
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 ) )
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 ) )
A5: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
A6: dom (Carrier F) = Seg n by PARTFUN1:def 2;
dom x = Seg n by A5, PARTFUN1:def 2;
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 & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;
hence x . i in the carrier of (F . i) by A6, A5, CARD_3:9; :: 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 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: 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 A5, CARD_3:9, FINSEQ_2:12, PARTFUN1:def 2; :: 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 (product F) ex y being Element of G st S1[x,y]
proof
let x be Element of (product F); :: thesis: ex y being Element of G st S1[x,y]
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)
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 15;
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 A11, FINSEQ_1:def 3;
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 A13, A14; :: thesis: verum
end;
consider f being Function of (product F),G such that
A15: for x being Element of the carrier of (product F) holds S1[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)
proof
let a, b be Element of (product F); :: thesis: f . (a * b) = (f . a) * (f . b)
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;
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 & (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: 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 A18, A22, A23, GROUP_4:17; :: thesis: verum
end;
then reconsider f = f as Homomorphism of (product F),G by GROUP_6:def 6;
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 :: 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 F) = product (Carrier F) by GROUP_7:def 2;
A26: dom s = Seg n by A24, FINSEQ_1:def 3;
A27: dom (Carrier F) = Seg n by PARTFUN1:def 2;
A28: for x being object st x in dom (Carrier F) holds
s . x in (Carrier F) . x
proof
let x be object ; :: 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 ;
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: verum
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: verum
end;
then A30: the carrier of G c= rng f by TARSKI:def 3;
rng f = the carrier of G by A30, XBOOLE_0:def 10;
then A31: f is onto by FUNCT_2:def 3;
for x1, x2 being object 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 object ; :: thesis: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 implies x1 = x2 )
assume A32: ( 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
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: verum
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: verum