thus ( f is non-decreasing implies for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n ) by VALUED_0:def 15; :: thesis: ( ( for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n ) implies f is non-decreasing )
assume A3: for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n ; :: thesis: f is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def 15 :: thesis: for b₁ being set holds
( not e1 in proj1 f or not b₁ in proj1 f or not e1 <= b₁ or f . e1 <= f . b₁ )
let e2 be ext-real number ; :: thesis: ( not e1 in proj1 f or not e2 in proj1 f or not e1 <= e2 or f . e1 <= f . e2 )
dom f c= NAT by RELAT_1:def 18;
hence ( not e1 in proj1 f or not e2 in proj1 f or not e1 <= e2 or f . e1 <= f . e2 ) by A3; :: thesis: verum