theorem Th8: :: INT_3:8

for n being Nat st n > 0 holds
for a, b being Element of Segm n
for k being Nat holds
( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) )