let n be non zero Nat; :: thesis: for G, F being Group-like associative commutative multMagma-Family of Seg n st ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) holds

ex f being Homomorphism of (product F),(product G) st

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product 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, F be Group-like associative commutative multMagma-Family of Seg n; :: thesis: ( ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) implies ex f being Homomorphism of (product F),(product G) st

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st

( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) )

assume A1: for k being Element of Seg n holds F . k = ProjGroup (G,k) ; :: thesis: ex f being Homomorphism of (product F),(product G) st

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st

( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )

A2: for i being Element of Seg n holds F . i is Subgroup of product G

( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )

s = t

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product 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 A2, A3, Th12; :: thesis: verum

ex f being Homomorphism of (product F),(product G) st

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product 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, F be Group-like associative commutative multMagma-Family of Seg n; :: thesis: ( ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) implies ex f being Homomorphism of (product F),(product G) st

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st

( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) )

assume A1: for k being Element of Seg n holds F . k = ProjGroup (G,k) ; :: thesis: ex f being Homomorphism of (product F),(product G) st

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st

( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )

A2: for i being Element of Seg n holds F . i is Subgroup of product G

proof

A3:
for x being Element of (product G) ex s being FinSequence of (product G) st
let i be Element of Seg n; :: thesis: F . i is Subgroup of product G

F . i = ProjGroup (G,i) by A1;

hence F . i is Subgroup of product G ; :: thesis: verum

end;F . i = ProjGroup (G,i) by A1;

hence F . i is Subgroup of product G ; :: thesis: verum

( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )

proof

for s, t being FinSequence of (product 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
let x be Element of (product G); :: thesis: ex s being FinSequence of (product G) st

( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )

consider s being FinSequence of (product G) such that

A4: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (G,k) ) & x = Product s ) by Th11;

take s ; :: thesis: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )

for k being Element of Seg n holds s . k in F . k

end;( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )

consider s being FinSequence of (product G) such that

A4: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (G,k) ) & x = Product s ) by Th11;

take s ; :: thesis: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )

for k being Element of Seg n holds s . k in F . k

proof

hence
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )
by A4; :: thesis: verum
let k be Element of Seg n; :: thesis: s . k in F . k

s . k in ProjGroup (G,k) by A4;

hence s . k in F . k by A1; :: thesis: verum

end;s . k in ProjGroup (G,k) by A4;

hence s . k in F . k by A1; :: thesis: verum

s = t

proof

hence
ex f being Homomorphism of (product F),(product G) st
let s, t be FinSequence of (product G); :: thesis: ( 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 implies s = t )

assume A5: ( 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 ) ; :: thesis: s = t

for k being Element of Seg n holds

( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) )

end;assume A5: ( 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 ) ; :: thesis: s = t

for k being Element of Seg n holds

( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) )

proof

hence
s = t
by A5, Th10; :: thesis: verum
let k be Element of Seg n; :: thesis: ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) )

( s . k in F . k & t . k in F . k ) by A5;

hence ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) ) by A1; :: thesis: verum

end;( s . k in F . k & t . k in F . k ) by A5;

hence ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) ) by A1; :: thesis: verum

( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product 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 A2, A3, Th12; :: thesis: verum