theorem Th34: :: INT_6:34

for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i