theorem Th20: :: GROUP_14:20

for m being CR_Sequence
for X being Group-Sequence
for I being Function of (Z/Z (Product m)),(product X) 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 ) ) & ( for x being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) ) holds
I is one-to-one