theorem :: REAL_3:24

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