for s being non empty increasing FinSequence of REAL
for r being Real st s . (len s) < r holds
s ^ <*r*> is non empty increasing FinSequence of REAL