theorem :: FRECHET2:38

for n0 being Element of NAT ex NS being increasing sequence of NAT st
for n being Element of NAT holds NS . n = n + n0