let s1, s2 be non empty increasing FinSequence of REAL ; :: thesis: for r being Real st s1 . (len s1) < r & r < s2 . 1 holds
(s1 ^ <*r*>) ^ s2 is non empty increasing FinSequence of REAL
let r be Real; :: thesis: ( s1 . (len s1) < r & r < s2 . 1 implies (s1 ^ <*r*>) ^ s2 is non empty increasing FinSequence of REAL )
assume A1: ( s1 . (len s1) < r & r < s2 . 1 ) ; :: thesis: (s1 ^ <*r*>) ^ s2 is non empty increasing FinSequence of REAL
then reconsider s = s1 ^ <*r*> as non empty increasing FinSequence of REAL by Th38;
s . (len s) = s . ((len s1) + 1) by FINSEQ_2:16
.= r by FINSEQ_1:42 ;
hence (s1 ^ <*r*>) ^ s2 is non empty increasing FinSequence of REAL by A1, Th1; :: thesis: verum