theorem Th14: :: INTEGR23:12

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