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:8;
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 dom IT or not b₁ in dom IT or not m <= b₁ or IT . b₁ <= IT . m )
let n be Element of NAT ; :: 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 and
A6: m <= n ; :: thesis: IT . n <= IT . m
defpred S₂[ Nat] means ( $1 in dom IT & m <= $1 implies IT . m >= IT . $1 );
A7: S₂[ 0 ] by FINSEQ_3:26;
A8: 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
A9: S₂[k] and
A10: 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 A11: ( m < k + 1 or m = k + 1 ) by XXREAL_0:1;

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

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

1 <= m by A4, FINSEQ_3:27;
then A13: 1 <= k by A12, XXREAL_0:2;
A14: k + 0 <= k + 1 by XREAL_1:8;
k + 1 <= len IT by A10, FINSEQ_3:27;
then A15: k <= len IT by A14, XXREAL_0:2;
then k in dom IT by A13, FINSEQ_3:27;
then IT . k >= IT . (k + 1) by A3, A10;
hence IT . m >= IT . (k + 1) by A9, A12, A13, A15, FINSEQ_3:27, 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;

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