theorem :: REAL_3:23

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