let m be CR_Sequence; :: thesis: for X being Group-Sequence
for I being Function of (Z/Z ()),() 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 ()) 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 ()),() 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 ()) holds
I . x = mod (x,m) ) holds
I is one-to-one

let I be Function of (Z/Z ()),(); :: 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 ()) 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 ()) 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 ()) & x2 in the carrier of (Z/Z ()) & I . x1 = I . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in the carrier of (Z/Z ()) & x2 in the carrier of (Z/Z ()) & I . x1 = I . x2 implies x1 = x2 )
assume A2: ( x1 in the carrier of (Z/Z ()) & x2 in the carrier of (Z/Z ()) & I . x1 = I . x2 ) ; :: thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Integer ;
A3: ( 0 <= xx1 & xx1 < Product m ) by ;
A4: ( 0 <= xx2 & xx2 < Product m ) by ;
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 ;
then A10: m . i > 0 by PARTFUN3:def 1;
A11: xx1 mod (m . i) = (mod (xx1,m)) . i by
.= (mod (xx2,m)) . i by A1, A2, A5
.= xx2 mod (m . i) by ;
then A12: m . i divides (xx1 - xx2) - I0 by ;
A13: m . i divides (xx2 - xx1) - I0 by ;
u . i = I0 ;
hence ( xx1 - xx2,u . i are_congruent_mod m . i & xx2 - xx1,u . i are_congruent_mod m . i ) by ; :: 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 ; :: thesis: verum
end;
A16: ( xx1 mod () >= 0 & xx1 mod () < Product m ) by NAT_D:62;
A17: ( xx2 mod () >= 0 & xx2 mod () < Product m ) by NAT_D:62;
A18: xx1 mod () = xx1 by ;
A19: xx2 mod () = xx2 by ;
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 () by ;
then (xx1 - xx2) - () < (xx1 mod ()) - (xx1 mod ()) by ;
then A21: xx1 - xx2 < (xx1 - xx2) - ((xx1 - xx2) - ()) 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 ;
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 () by ;
then (xx2 - xx1) - () < (xx2 mod ()) - (xx2 mod ()) by ;
then A23: xx2 - xx1 < (xx2 - xx1) - ((xx2 - xx1) - ()) 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 ;
hence x1 = x2 ; :: thesis: verum
end;
end;
end;
hence I is one-to-one by FUNCT_2:19; :: thesis: verum