thus
( IT is non-increasing implies for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1) ) :: thesis: ( ( for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1) ) implies IT is non-increasing )

IT . n >= IT . (n + 1) ; :: thesis: IT is non-increasing

let m, n be Nat; :: according to SEQM_3:def 4 :: thesis: ( not m in dom IT or not n in dom IT or not m <= n or IT . n <= IT . m )

assume that

A4: m in dom IT and

A5: ( n in dom IT & m <= n ) ; :: thesis: IT . n <= IT . m

defpred S_{2}[ Nat] means ( $1 in dom IT & m <= $1 implies IT . m >= IT . $1 );

A6: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]
_{2}[ 0 ]
by FINSEQ_3:24;

for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A13, A6);

hence IT . n <= IT . m by A5; :: thesis: verum

IT . n >= IT . (n + 1) ) :: thesis: ( ( for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1) ) implies IT is non-increasing )

proof

assume A3:
for n being Nat st n in dom IT & n + 1 in dom IT holds
assume A1:
IT is non-increasing
; :: thesis: for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1)

let n be Nat; :: thesis: ( n in dom IT & n + 1 in dom IT implies IT . n >= IT . (n + 1) )

assume A2: ( n in dom IT & n + 1 in dom IT ) ; :: thesis: IT . n >= IT . (n + 1)

n + 0 <= n + 1 by XREAL_1:6;

hence IT . n >= IT . (n + 1) by A1, A2; :: thesis: verum

end;IT . n >= IT . (n + 1)

let n be Nat; :: thesis: ( n in dom IT & n + 1 in dom IT implies IT . n >= IT . (n + 1) )

assume A2: ( n in dom IT & n + 1 in dom IT ) ; :: thesis: IT . n >= IT . (n + 1)

n + 0 <= n + 1 by XREAL_1:6;

hence IT . n >= IT . (n + 1) by A1, A2; :: thesis: verum

IT . n >= IT . (n + 1) ; :: thesis: IT is non-increasing

let m, n be Nat; :: according to SEQM_3:def 4 :: thesis: ( not m in dom IT or not n in dom IT or not m <= n or IT . n <= IT . m )

assume that

A4: m in dom IT and

A5: ( n in dom IT & m <= n ) ; :: thesis: IT . n <= IT . m

defpred S

A6: for k being Nat st S

S

proof

A13:
S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume that

A7: S_{2}[k]
and

A8: k + 1 in dom IT ; :: thesis: ( not m <= k + 1 or IT . m >= IT . (k + 1) )

assume m <= k + 1 ; :: thesis: IT . m >= IT . (k + 1)

then A9: ( m < k + 1 or m = k + 1 ) by XXREAL_0:1;

end;assume that

A7: S

A8: k + 1 in dom IT ; :: thesis: ( not m <= k + 1 or IT . m >= IT . (k + 1) )

assume m <= k + 1 ; :: thesis: IT . m >= IT . (k + 1)

then A9: ( m < k + 1 or m = k + 1 ) by XXREAL_0:1;

per cases
( m <= k or m = k + 1 )
by A9, NAT_1:13;

end;

suppose A10:
m <= k
; :: thesis: IT . m >= IT . (k + 1)

( k + 0 <= k + 1 & k + 1 <= len IT )
by A8, FINSEQ_3:25, XREAL_1:6;

then A11: k <= len IT by XXREAL_0:2;

1 <= m by A4, FINSEQ_3:25;

then A12: 1 <= k by A10, XXREAL_0:2;

then k in dom IT by A11, FINSEQ_3:25;

then IT . k >= IT . (k + 1) by A3, A8;

hence IT . m >= IT . (k + 1) by A7, A10, A12, A11, FINSEQ_3:25, XXREAL_0:2; :: thesis: verum

end;then A11: k <= len IT by XXREAL_0:2;

1 <= m by A4, FINSEQ_3:25;

then A12: 1 <= k by A10, XXREAL_0:2;

then k in dom IT by A11, FINSEQ_3:25;

then IT . k >= IT . (k + 1) by A3, A8;

hence IT . m >= IT . (k + 1) by A7, A10, A12, A11, FINSEQ_3:25, XXREAL_0:2; :: thesis: verum

for k being Nat holds S

hence IT . n <= IT . m by A5; :: thesis: verum