let m be 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
let X be 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 I be Function of (Z/Z (Product m)),(product X); ( 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) ) )
; 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 ;
( 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 )
;
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 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;
( 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
;
( 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;
verum end;
A14:
for
i being
Nat st
i in dom m holds
I0,
u . i are_congruent_mod m . i
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;
end;
hence
I is one-to-one
by FUNCT_2:19; verum