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 0 < n ;
then A2: 0 + 1 <= n by NAT_1:13;
now
per cases ( len f <= n or n < len f ) ;
case n < len f ; :: thesis: f | n is non-decreasing FinSequence of REAL
then A3: ( n in dom f & len (f | n) = n ) by A2, 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) )
assume A4: ( m in dom (f | n) & m + 1 in dom (f | n) ) ; :: thesis: (f | n) . m <= (f | n) . (m + 1)
( dom f = Seg (len f) & dom (f | n) = Seg (len (f | n)) ) by FINSEQ_1:def 3;
then ( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) & m in dom f & m + 1 in dom f ) by A3, A4, RFINSEQ:19;
hence (f | n) . m <= (f | n) . (m + 1) by 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