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

proof

let x1, x2 be object ; :: thesis: ( x1 in the carrier of (Z/Z (Product m)) & x2 in the carrier of (Z/Z (Product m)) & I . x1 = I . x2 implies x1 = x2 )
assume A2: ( x1 in the carrier of (Z/Z (Product m)) & x2 in the carrier of (Z/Z (Product m)) & I . x1 = I . x2 ) ; :: thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Integer ;
A3: ( 0 <= xx1 & xx1 < Product m ) by A2, NAT_1:44;
A4: ( 0 <= xx2 & xx2 < Product m ) by A2, NAT_1:44;
A5: I . x2 = mod (xx2,m) by A1, A2;
reconsider I0 = 0 as Integer ;
reconsider u = {} as INT -valued FinSequence ;
A6: dom (mod (xx1,m)) = Seg (len (mod (xx1,m))) by FINSEQ_1:def 3
.= Seg (len m) by INT_6:def 3
.= dom m by FINSEQ_1:def 3 ;

A7: now :: thesis: for i being Nat st i in dom m holds
( xx1 - xx2,u . i are_congruent_mod m . i & xx2 - xx1,u . i are_congruent_mod m . i )

let i be Nat; :: thesis: ( i in dom m implies ( xx1 - xx2,u . i are_congruent_mod m . i & xx2 - xx1,u . i are_congruent_mod m . i ) )
assume A8: i in dom m ; :: thesis: ( xx1 - xx2,u . i are_congruent_mod m . i & xx2 - xx1,u . i are_congruent_mod m . i )
A9: i in dom (mod (xx2,m)) by A5, A6, A1, A2, A8;
m . i in rng m by FUNCT_1:3, A8;
then A10: m . i > 0 by PARTFUN3:def 1;
A11: xx1 mod (m . i) = (mod (xx1,m)) . i by A6, A8, INT_6:def 3
.= (mod (xx2,m)) . i by A1, A2, A5
.= xx2 mod (m . i) by A9, INT_6:def 3 ;
then A12: m . i divides (xx1 - xx2) - I0 by INT_1:def 4, NAT_D:64, A10;
A13: m . i divides (xx2 - xx1) - I0 by INT_1:def 4, NAT_D:64, A10, A11;
u . i = I0 ;
hence ( xx1 - xx2,u . i are_congruent_mod m . i & xx2 - xx1,u . i are_congruent_mod m . i ) by A12, A13, INT_1:def 4; :: thesis: verum

end;

A14: for i being Nat st i in dom m holds
I0,u . i are_congruent_mod m . i

proof

let i be Nat; :: thesis: ( i in dom m implies I0,u . i are_congruent_mod m . i )
assume i in dom m ; :: thesis: I0,u . i are_congruent_mod m . i
A15: u . i = I0 ;
I0 - I0 = (I0 - I0) * (m . i) ;
hence I0,u . i are_congruent_mod m . i by A15, INT_1:def 4, INT_1:def 3; :: thesis: verum

end;

A16: ( xx1 mod (Product m) >= 0 & xx1 mod (Product m) < Product m ) by NAT_D:62;
A17: ( xx2 mod (Product m) >= 0 & xx2 mod (Product m) < Product m ) by NAT_D:62;
A18: xx1 mod (Product m) = xx1 by A3, NAT_D:63;
A19: xx2 mod (Product m) = xx2 by A4, NAT_D:63;

per cases ( xx2 <= xx1 or not xx2 <= xx1 ) ;

suppose xx2 <= xx1 ; :: thesis: x1 = x2

then A20: xx1 - xx2 in NAT by INT_1:5;
xx1 - xx2 <= xx1 mod (Product m) by A18, XREAL_1:43, A2;
then (xx1 - xx2) - (Product m) < (xx1 mod (Product m)) - (xx1 mod (Product m)) by A16, XREAL_1:15;
then A21: xx1 - xx2 < (xx1 - xx2) - ((xx1 - xx2) - (Product m)) by XREAL_1:46;
for i being Nat st i in dom m holds
xx1 - xx2,u . i are_congruent_mod m . i by A7;
then xx1 - xx2 = I0 by INT_6:42, A14, A20, A21;
hence x1 = x2 ; :: thesis: verum

end;

suppose not xx2 <= xx1 ; :: thesis: x1 = x2

then A22: xx2 - xx1 in NAT by INT_1:5;
xx2 - xx1 <= xx2 mod (Product m) by A19, XREAL_1:43, A2;
then (xx2 - xx1) - (Product m) < (xx2 mod (Product m)) - (xx2 mod (Product m)) by A17, XREAL_1:15;
then A23: xx2 - xx1 < (xx2 - xx1) - ((xx2 - xx1) - (Product m)) by XREAL_1:46;
for i being Nat st i in dom m holds
xx2 - xx1,u . i are_congruent_mod m . i by A7;
then xx2 - xx1 = I0 by INT_6:42, A14, A22, A23;
hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence I is one-to-one by FUNCT_2:19; :: thesis: verum