let s be non empty increasing FinSequence of REAL ; :: thesis: for r being Real st s . (len s) < r holds
s ^ <*r*> is non empty increasing FinSequence of REAL
let r be Real; :: thesis: ( s . (len s) < r implies s ^ <*r*> is non empty increasing FinSequence of REAL )
assume s . (len s) < r ; :: thesis: s ^ <*r*> is non empty increasing FinSequence of REAL
then s . (len s) < <*r*> . 1 by FINSEQ_1:def 8;
hence s ^ <*r*> is non empty increasing FinSequence of REAL by Th1; :: thesis: verum