thus ( IT is non-increasing implies for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) ) :: thesis: ( ( for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) ) implies IT is non-increasing )

proof

assume A1: IT is non-increasing ; :: thesis: for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1)
let n be Element of 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, SEQM_3:def 4; :: thesis: verum

end;

assume A3: for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) ; :: thesis: IT is non-increasing
let m be Element of NAT ; :: according to SEQM_3:def 4 :: thesis: for b₁ being Element of NAT holds
( not m in proj1 IT or not b₁ in proj1 IT or not m <= b₁ or IT . b₁ <= IT . m )
let n be Element of NAT ; :: thesis: ( not m in proj1 IT or not n in proj1 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₂[ Nat] means ( $1 in dom IT & m <= $1 implies IT . m >= IT . $1 );
A6: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume that
A7: S₂[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;

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

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;

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

hence IT . m >= IT . (k + 1) ; :: thesis: verum

end;

end;

end;

A13: S₂[ 0 ] by FINSEQ_3:24;
for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A13, A6);
hence IT . n <= IT . m by A5; :: thesis: verum