let f be non-increasing FinSequence of REAL ; :: thesis: for n being Nat holds f | n is non-increasing FinSequence of REAL

let n be Nat; :: thesis: f | n is non-increasing FinSequence of REAL

set fn = f | n;

let n be Nat; :: thesis: f | n is non-increasing FinSequence of REAL

set fn = f | n;

now :: thesis: ( ( n = 0 & f | n is non-increasing FinSequence of REAL ) or ( n <> 0 & f | n is non-increasing FinSequence of REAL ) )end;

hence
f | n is non-increasing FinSequence of REAL
; :: thesis: verumper cases
( n = 0 or n <> 0 )
;

end;

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

then
0 < n
;

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

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

now :: thesis: ( ( len f <= n & f | n is non-increasing FinSequence of REAL ) or ( n < len f & f | n is non-increasing FinSequence of REAL ) )end;

hence
f | n is non-increasing FinSequence of REAL
; :: thesis: verumper cases
( len f <= n or n < len f )
;

end;

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

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

end;now :: thesis: for m being Nat st m in dom (f | n) & m + 1 in dom (f | n) holds

(f | n) . m >= (f | n) . (m + 1)

hence
f | n is non-increasing FinSequence of REAL
by Def3; :: thesis: verum(f | n) . m >= (f | n) . (m + 1)

let m be 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, Th6;

( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, Th6;

hence (f | n) . m >= (f | n) . (m + 1) by A5, Def3; :: thesis: verum

end;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, Th6;

( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, Th6;

hence (f | n) . m >= (f | n) . (m + 1) by A5, Def3; :: thesis: verum