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 A: ( 0 <= u * v & u * v < Product m ) ; :: thesis: to_int ((mod u,m) (#) (mod v,m)),m = u * v
A1: len (mod (u * v),m) = len m by Df1;
A2: for i being natural number st i in dom m holds
u * v,(mod (u * v),m) . i are_congruent_mod m . i by lemat4;
set z = to_int ((mod u,m) (#) (mod v,m)),m;
len (mod v,m) = len m by Df1;
then ( len (mod u,m) = len (mod v,m) & len (mod u,m) = len m ) by Df1;
then len ((mod u,m) (#) (mod v,m)) = len m by length3;
then A3: ( 0 <= to_int ((mod u,m) (#) (mod v,m)),m & to_int ((mod u,m) (#) (mod v,m)),m < Product m ) by lemat2;
A4: 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 B0: i in dom m ; :: thesis: to_int ((mod u,m) (#) (mod v,m)),m,(mod (u * v),m) . i are_congruent_mod m . i
dom (mod (u * v),m) = Seg (len m) by A1, FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
then B1: (mod (u * v),m) . i = (u * v) mod (m . i) by B0, Df1;
to_int ((mod u,m) (#) (mod v,m)),m,u * v are_congruent_mod m . i by B0, lemat3;
then B3: (to_int ((mod u,m) (#) (mod v,m)),m) mod (m . i) = (u * v) mod (m . i) by INT_3:12;
m . i in rng m by B0, FUNCT_1:12;
then D1: 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 B1, D1, B3, INT_3:12; :: thesis: verum

end;

thus to_int ((mod u,m) (#) (mod v,m)),m = u * v by A, A2, A3, A4, Th3; :: thesis: verum