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

let n be Nat; :: thesis: ( n is Element of NAT implies f /^ n is non-increasing )

set fn = f /^ n;

let n be Nat; :: thesis: ( n is Element of NAT implies f /^ n is non-increasing )

set fn = f /^ n;

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
( n is Element of NAT implies f /^ n is non-increasing )
; :: 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) )

assume that

A1: m in dom (f /^ n) and

A2: m + 1 in dom (f /^ n) ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)

A3: m <= m + n by NAT_1:11;

1 <= m by A1, FINSEQ_3:25;

then A4: 1 <= m + n by A3, XXREAL_0:2;

A5: 1 <= (m + n) + 1 by NAT_1:11;

A6: m + 1 <= len (f /^ n) by A2, FINSEQ_3:25;

set r = (f /^ n) . m;

set s = (f /^ n) . (m + 1);

A7: (m + 1) + n = (m + n) + 1 ;

A8: m <= len (f /^ n) by A1, FINSEQ_3:25;

end;assume that

A1: m in dom (f /^ n) and

A2: m + 1 in dom (f /^ n) ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)

A3: m <= m + n by NAT_1:11;

1 <= m by A1, FINSEQ_3:25;

then A4: 1 <= m + n by A3, XXREAL_0:2;

A5: 1 <= (m + n) + 1 by NAT_1:11;

A6: m + 1 <= len (f /^ n) by A2, FINSEQ_3:25;

set r = (f /^ n) . m;

set s = (f /^ n) . (m + 1);

A7: (m + 1) + n = (m + n) + 1 ;

A8: m <= len (f /^ n) by A1, FINSEQ_3:25;

now :: thesis: ( ( n <= len f & (f /^ n) . m >= (f /^ n) . (m + 1) ) or ( len f < n & (f /^ n) . m >= (f /^ n) . (m + 1) ) )end;

hence
(f /^ n) . m >= (f /^ n) . (m + 1)
; :: thesis: verumper cases
( n <= len f or len f < n )
;

end;

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

then A10:
len (f /^ n) = (len f) - n
by Def1;

then m + n <= len f by A8, XREAL_1:19;

then A11: m + n in dom f by A4, FINSEQ_3:25;

(m + n) + 1 <= len f by A6, A7, A10, XREAL_1:19;

then A12: (m + n) + 1 in dom f by A5, FINSEQ_3:25;

( (f /^ n) . m = f . (m + n) & (f /^ n) . (m + 1) = f . ((m + n) + 1) ) by A1, A2, A7, A9, Def1;

hence (f /^ n) . m >= (f /^ n) . (m + 1) by A11, A12, Def3; :: thesis: verum

end;then m + n <= len f by A8, XREAL_1:19;

then A11: m + n in dom f by A4, FINSEQ_3:25;

(m + n) + 1 <= len f by A6, A7, A10, XREAL_1:19;

then A12: (m + n) + 1 in dom f by A5, FINSEQ_3:25;

( (f /^ n) . m = f . (m + n) & (f /^ n) . (m + 1) = f . ((m + n) + 1) ) by A1, A2, A7, A9, Def1;

hence (f /^ n) . m >= (f /^ n) . (m + 1) by A11, A12, Def3; :: thesis: verum