let m be CR_Sequence; :: thesis: for X being Group-Sequence st len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) holds
ex I being Homomorphism of (Z/Z (Product m)),(product X) st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) ) )
let X be Group-Sequence; :: thesis: ( len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) implies ex I being Homomorphism of (Z/Z (Product m)),(product X) st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) ) ) )
assume A1: ( len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) ) ; :: thesis: ex I being Homomorphism of (Z/Z (Product m)),(product X) st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) ) )
then consider I being Homomorphism of (Z/Z (Product m)),(product X) such that
A2: for x being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) by Th14;
A3: I is one-to-one by A1, Th20, A2;
Product m is Nat by TARSKI:1;
then A4: card (Segm (Product m)) = Product m ;
A5: card the carrier of (product X) = Product m by A1, Th19;
then the carrier of (product X) is finite ;
then I is onto by A3, A4, A5, FINSEQ_4:63;
hence ex I being Homomorphism of (Z/Z (Product m)),(product X) st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) ) ) by A2, A3; :: thesis: verum