thus ( f is 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 14; :: 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 decreasing )
assume Z: 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 decreasing
let e1 be ext-real number ; :: according to VALUED_0:def 14 :: thesis: for b₁ being set holds
( not e1 in dom f or not b₁ in dom f or b₁ <= e1 or not f . e1 <= f . b₁ )
let e2 be ext-real number ; :: thesis: ( not e1 in dom f or not e2 in dom f or e2 <= e1 or not f . e1 <= f . e2 )
dom f c= NAT by RELAT_1:def 18;
hence ( not e1 in dom f or not e2 in dom f or e2 <= e1 or not f . e1 <= f . e2 ) by Z; :: thesis: verum