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 )
proof
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;
assume A3: for n being Nat st n in dom IT & n + 1 in dom IT holds
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 S2[ Nat] means ( $1 in dom IT & m <= $1 implies IT . m >= IT . $1 );
A6: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume that
A7: S2[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 m = k + 1 ; :: thesis: IT . m >= IT . (k + 1)
hence IT . m >= IT . (k + 1) ; :: thesis: verum
end;
end;
end;
A13: S2[ 0 ] by FINSEQ_3:24;
for k being Nat holds S2[k] from NAT_1:sch 2(A13, A6);
 hence IT . n <= IT . m by A5; :: thesis: verum