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 A2: len (s | m) = m by FINSEQ_1:59;
set H = s | m;
for e1, e2 being ExtReal st e1 in dom (s | m) & e2 in dom (s | m) & e1 < e2 holds
(s | m) . e1 < (s | m) . e2
proof
let e1, e2 be ExtReal; :: thesis: ( e1 in dom (s | m) & e2 in dom (s | m) & e1 < e2 implies (s | m) . e1 < (s | m) . e2 )
assume A3: ( e1 in dom (s | m) & e2 in dom (s | m) & e1 < e2 ) ; :: thesis: (s | m) . e1 < (s | m) . e2
then A5: ( e1 in dom s & e2 in dom s ) by RELAT_1:57;
( s . e1 = (s | m) . e1 & s . e2 = (s | m) . e2 ) by A3, FUNCT_1:47;
hence (s | m) . e1 < (s | m) . e2 by A3, A5, VALUED_0:def 13; :: thesis: verum
end;
hence s | m is non empty increasing FinSequence of REAL by A2, VALUED_0:def 13, a0, FINSEQ_3:25; :: thesis: verum