thus ( s is non-decreasing implies for n being Nat holds s . n <= s . (n + 1) ) :: thesis: ( ( for n being Nat holds s . n <= s . (n + 1) ) implies s is non-decreasing )

proof

assume A1: s is non-decreasing ; :: thesis: for n being Nat holds s . n <= s . (n + 1)
let n be Nat; :: thesis: s . n <= s . (n + 1)
A2: dom s = NAT by FUNCT_2:def 1;
A3: ( n in NAT & n + 1 in NAT ) by ORDINAL1:def 13;
n < n + 1 by NAT_1:13;
hence s . n <= s . (n + 1) by A1, A2, VALUED_0:def 15, A3; :: thesis: verum

end;

assume A3: for n being Nat holds s . n <= s . (n + 1) ; :: thesis: s is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def 15 :: thesis: for b₁ being set holds
( not e1 in dom s or not b₁ in dom s or not e1 <= b₁ or s . e1 <= s . b₁ )
let e2 be ext-real number ; :: thesis: ( not e1 in dom s or not e2 in dom s or not e1 <= e2 or s . e1 <= s . e2 )
assume ( e1 in dom s & e2 in dom s ) ; :: thesis: ( not e1 <= e2 or s . e1 <= s . e2 )
then reconsider m = e1, n = e2 as Nat ;
assume Z: e1 <= e2 ; :: thesis: s . e1 <= s . e2
defpred S₁[ Nat] means ( m <= $1 implies s . m <= s . $1 );
A: S₁[ 0 ] ;
B: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume z: S₁[j] ; :: thesis: S₁[j + 1]
assume m <= j + 1 ; :: thesis: s . m <= s . (j + 1)
then C: ( m < j + 1 or m = j + 1 ) by XXREAL_0:1;
s . j <= s . (j + 1) by A3;
hence s . m <= s . (j + 1) by C, XXREAL_0:2, z, NAT_1:13; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A, B);
then s . m <= s . n by Z;
hence s . e1 <= s . e2 ; :: thesis: verum