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

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 A1: ( m in dom (f /^ n) & m + 1 in dom (f /^ n) ) ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)
then A2: ( 1 <= m & m <= len (f /^ n) & 1 <= m + 1 & m + 1 <= len (f /^ n) ) by FINSEQ_3:27;
A3: ( (m + 1) + n = (m + n) + 1 & m <= m + n & m + 1 <= (m + 1) + n ) by NAT_1:11;
then A4: ( 1 <= m + n & 1 <= (m + n) + 1 & 1 <= len (f /^ n) ) by A2, XXREAL_0:2;
set r = (f /^ n) . m;
set s = (f /^ n) . (m + 1);

now

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

case n <= len f ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)

then A5: ( len (f /^ n) = (len f) - n & (f /^ n) . m = f . (m + n) & (f /^ n) . (m + 1) = f . ((m + n) + 1) ) by A1, A3, Def2;
then ( m + n <= len f & (m + n) + 1 <= len f ) by A2, A3, XREAL_1:21;
then ( m + n in dom f & (m + n) + 1 in dom f ) by A4, FINSEQ_3:27;
hence (f /^ n) . m >= (f /^ n) . (m + 1) by A5, Def4; :: thesis: verum

end;

case len f < n ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)

then f /^ n = <*> REAL by Def2;
hence (f /^ n) . m >= (f /^ n) . (m + 1) by A1; :: thesis: verum

end;

end;

end;

hence (f /^ n) . m >= (f /^ n) . (m + 1) ; :: thesis: verum

end;

hence f /^ n is non-increasing FinSequence of REAL by Def4; :: thesis: verum