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

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

hence
I is one-to-one
by FUNCT_2:19; :: thesis: verum
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 ;

I0,u . i are_congruent_mod m . i

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;

end;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 )

A14:
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;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

I0,u . i are_congruent_mod m . i

proof

A16:
( xx1 mod (Product m) >= 0 & xx1 mod (Product m) < Product m )
by NAT_D:62;
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;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

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 )
;

end;

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;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

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;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