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
proof
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;
A3: for x being Element of (product G) 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 )
proof
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
proof
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;
hence ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) by A4; :: thesis: verum
end;
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
s = t
proof
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) )
proof
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;
hence s = t by A5, Th10; :: thesis: verum
end;
hence 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 ) ) ) by A2, A3, Th12; :: thesis: verum