let s be non empty increasing FinSequence of REAL ; :: thesis: for m being Nat st m in dom s holds
s | m is non empty increasing FinSequence of REAL
let m be Nat; :: thesis: ( m in dom s implies s | m is non empty increasing FinSequence of REAL )
assume a0: m in dom s ; :: thesis: s | m is non empty increasing FinSequence of REAL
then ( 1 <= m & m <= len s ) by FINSEQ_3:25;
then len (s | m) = m by FINSEQ_1:59;
hence s | m is non empty increasing FinSequence of REAL by a0, FINSEQ_3:25; :: thesis: verum