theorem :: GROUP_14:21

for m being CR_Sequence
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) ) )