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 ) )_{1}[ 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_{1}[x,y]

A15: for x being Element of the carrier of (product F) holds S_{1}[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)

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 ) ) )

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

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

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

defpred S
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)

s . i in the carrier of G

x . i in (Carrier F) . i ) ) by A5, CARD_3:9, FINSEQ_2:12, PARTFUN1:def 2; :: thesis: verum

end;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

for i being Nat st i in dom s holds
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 A6, A5, CARD_3:9; :: thesis: verum

end;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 A6, A5, CARD_3:9; :: thesis: verum

s . i in the carrier of G

proof

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
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;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

x . i in (Carrier F) . i ) ) by A5, CARD_3:9, FINSEQ_2:12, PARTFUN1:def 2; :: thesis: verum

( 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

proof

consider f being Function of (product F),G such that
let x be Element of (product F); :: thesis: ex y being Element of G st S_{1}[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)

then A13: len s = n by A11, FINSEQ_1:def 3;

_{1}[x, Product s]

thus S_{1}[x, Product s]
by A13, A14; :: thesis: verum

end;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

n in NAT
by ORDINAL1:def 12;
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 A10; :: thesis: verum

end;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 A10; :: thesis: verum

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

take
Product s
; :: thesis: Slet 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;s . k in the carrier of (F . k) by A12;

hence s . k in F . k by STRUCT_0:def 5; :: thesis: verum

thus S

A15: for x being Element of the carrier of (product F) holds S

for a, b being Element of (product F) holds f . (a * b) = (f . a) * (f . b)

proof

then reconsider f = f as Homomorphism of (product F),G by GROUP_6:def 6;
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;

( 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;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)

A22:
ex sa being FinSequence of G st 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 13;

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 13;

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;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 13;

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 13;

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

( 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

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

then A30:
the carrier of G c= rng f
by TARSKI:def 3;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

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;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

reconsider x = s as Element of (product F) by A25, A26, A27, A28, CARD_3:9;
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 13;

hence s . x in (Carrier F) . x by A29, STRUCT_0:def 5; :: thesis: verum

end;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 13;

hence s . x in (Carrier F) . x by A29, STRUCT_0:def 5; :: thesis: verum

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

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

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

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