let s be non empty increasing FinSequence of REAL ; :: thesis: for a being Real st s . (len s) < a holds
s ^ <*a*> is non empty increasing FinSequence of REAL
let a be Real; :: thesis: ( s . (len s) < a implies s ^ <*a*> is non empty increasing FinSequence of REAL )
assume A1: s . (len s) < a ; :: thesis: s ^ <*a*> is non empty increasing FinSequence of REAL
reconsider a0 = a as Element of REAL by XREAL_0:def 1;
reconsider t = <*a0*> as non empty increasing FinSequence of REAL ;
s . (len s) < t . 1 by A1, FINSEQ_1:40;
hence s ^ <*a*> is non empty increasing FinSequence of REAL by Th13; :: thesis: verum