theorem Th19: :: REAL_3:19

for n, m being Nat st n <> 0 holds
m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0)