theorem Th14: :: REAL_3:14

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