for p being Real
for a being Real_Sequence
for x0 being Real st ( for n being Nat holds a . n = x0 + (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )