let u, v be Integer; :: thesis: for m being CR_Sequence st 0 <= u - v & u - v < Product m holds
to_int ((mod u,m) - (mod v,m)),m = u - v
let m be CR_Sequence; :: thesis: ( 0 <= u - v & u - v < Product m implies to_int ((mod u,m) - (mod v,m)),m = u - v )
assume that
A1: 0 <= u - v and
A2: u - v < Product m ; :: thesis: to_int ((mod u,m) - (mod v,m)),m = u - v
set z = to_int ((mod u,m) - (mod v,m)),m;
A3: for i being natural number st i in dom m holds
u - v,(mod (u - v),m) . i are_congruent_mod m . i by Th32;
A4: len (mod (u - v),m) = len m by Def3;
A5: for i being natural number st i in dom m holds
to_int ((mod u,m) - (mod v,m)),m,(mod (u - v),m) . i are_congruent_mod m . i

proof

let i be natural number ; :: thesis: ( i in dom m implies to_int ((mod u,m) - (mod v,m)),m,(mod (u - v),m) . i are_congruent_mod m . i )
assume A6: i in dom m ; :: thesis: to_int ((mod u,m) - (mod v,m)),m,(mod (u - v),m) . i are_congruent_mod m . i
then to_int ((mod u,m) - (mod v,m)),m,u - v are_congruent_mod m . i by Th36;
then A7: (to_int ((mod u,m) - (mod v,m)),m) mod (m . i) = (u - v) mod (m . i) by INT_3:12;
dom (mod (u - v),m) = Seg (len m) by A4, FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
then A8: (mod (u - v),m) . i = (u - v) mod (m . i) by A6, Def3;
m . i in rng m by A6, FUNCT_1:12;
then A9: m . i > 0 by PARTFUN3:def 1;
then m . i is Element of NAT by INT_1:16;
then (u - v) mod (m . i) = ((u - v) mod (m . i)) mod (m . i) by INT_3:13;
hence to_int ((mod u,m) - (mod v,m)),m,(mod (u - v),m) . i are_congruent_mod m . i by A8, A7, A9, INT_3:12; :: thesis: verum

end;

A10: len (mod u,m) = len m by Def3;
len (mod v,m) = len m by Def3;
then A11: len ((mod u,m) - (mod v,m)) = len m by A10, Lm3;
then A12: to_int ((mod u,m) - (mod v,m)),m < Product m by Th31;
0 <= to_int ((mod u,m) - (mod v,m)),m by A11, Th31;
hence to_int ((mod u,m) - (mod v,m)),m = u - v by A1, A2, A3, A12, A5, Lm8; :: thesis: verum