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

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