theorem Th22: :: REAL_3:22

for m being Nat holds modSeq (m,0) = NAT --> 0