thus ( f is non-increasing 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 16; :: 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-increasing )
assume A4: 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-increasing
let e1 be ext-real number ; :: according to VALUED_0:def 16 :: thesis: for b₁ being set holds
( not e1 in proj1 f or not b₁ in proj1 f or not e1 <= b₁ or f . b₁ <= f . e1 )
let e2 be ext-real number ; :: thesis: ( not e1 in proj1 f or not e2 in proj1 f or not e1 <= e2 or f . e2 <= f . e1 )
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 . e2 <= f . e1 ) by A4; :: thesis: verum