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 ()),() st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z ()) 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 ()),() st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z ()) 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 ()),() st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z ()) holds
I . x = mod (x,m) ) )

then consider I being Homomorphism of (Z/Z ()),() such that
A2: for x being Integer st x in the carrier of (Z/Z ()) 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 ;
A5: card the carrier of () = Product m by ;
then the carrier of () is finite ;
then I is onto by ;
hence ex I being Homomorphism of (Z/Z ()),() st
( I is bijective & ( for x being Integer st x in the carrier of (Z/Z ()) holds
I . x = mod (x,m) ) ) by A2, A3; :: thesis: verum