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 Nat 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 Nat 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 Nat; :: 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 Th37;
then A7: (to_int (((mod (u,m)) (#) (mod (v,m))),m)) mod (m . i) = (u * v) mod (m . i) by NAT_D:64;
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:3;
then A9: m . i > 0 by PARTFUN3:def 1;
then m . i is Element of NAT by INT_1:3;
then (u * v) mod (m . i) = ((u * v) mod (m . i)) mod (m . i) by NAT_D:65;
hence to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i by A8, A7, A9, NAT_D:64; :: 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, Lm4;
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, Lm9; :: thesis: verum