theorem Th16: :: REAL_3:16

for a, n, m being Nat st (divSeq (m,n)) . (a + 1) = 0 holds
(modSeq (m,n)) . a = 0