theorem Th17: :: REAL_3:17

for a, b, n, m being Nat st a <> 0 & a <= b & (divSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . b = 0