let f be non-decreasing FinSequence of REAL ; :: thesis: for n being Element of NAT holds f | n is non-decreasing FinSequence of REAL
let n be Element of NAT ; :: thesis: f | n is non-decreasing FinSequence of REAL
set fn = f | n;

now

per cases ( n = 0 or n <> 0 ) ;

case n = 0 ; :: thesis: f | n is non-decreasing FinSequence of REAL

then len (f | n) = 0 ;
hence f | n is non-decreasing FinSequence of REAL by Th16; :: thesis: verum

end;

case n <> 0 ; :: thesis: f | n is non-decreasing FinSequence of REAL

then A1: 0 + 1 <= n by NAT_1:13;

now

per cases ( len f <= n or n < len f ) ;

case len f <= n ; :: thesis: f | n is non-decreasing FinSequence of REAL

hence f | n is non-decreasing FinSequence of REAL by FINSEQ_1:79; :: thesis: verum

end;

case n < len f ; :: thesis: f | n is non-decreasing FinSequence of REAL

then A2: ( n in dom f & len (f | n) = n ) by A1, FINSEQ_1:80, FINSEQ_3:27;

now

let m be Element of NAT ; :: thesis: ( m in dom (f | n) & m + 1 in dom (f | n) implies (f | n) . m <= (f | n) . (m + 1) )
A3: dom (f | n) = Seg (len (f | n)) by FINSEQ_1:def 3;
assume A4: ( m in dom (f | n) & m + 1 in dom (f | n) ) ; :: thesis: (f | n) . m <= (f | n) . (m + 1)
then A5: ( m in dom f & m + 1 in dom f ) by A2, A3, RFINSEQ:19;
( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, RFINSEQ:19;
hence (f | n) . m <= (f | n) . (m + 1) by A5, INTEGRA2:def 1; :: thesis: verum

end;

hence f | n is non-decreasing FinSequence of REAL by INTEGRA2:def 1; :: thesis: verum

end;

end;

end;

hence f | n is non-decreasing FinSequence of REAL ; :: thesis: verum

end;

end;

end;

hence f | n is non-decreasing FinSequence of REAL ; :: thesis: verum