for n being Nat
for seq being Real_Sequence st seq is V46() & rng seq c= NAT holds
n <= seq . n