theorem Th21: :: REAL_3:21

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