for r being Real st r in rng (f - (max f)) holds
r <= 0

proof

let r be Real; :: thesis: ( r in rng (f - (max f)) implies r <= 0 )
assume A1: r in rng (f - (max f)) ; :: thesis: r <= 0
consider x being object such that
A2: ( x in dom (f - (max f)) & r = (f - (max f)) . x ) by A1, FUNCT_1:def 3;
A3: ( dom (f - (max f)) = dom f & ( for i being object st i in dom f holds
(f - (max f)) . i = (f . i) - (max f) ) ) by VALUED_1:3;
reconsider x = x as Nat by A2;
( 1 <= x & x <= len f ) by A2, A3, FINSEQ_3:25;
then (f . x) - (max f) <= (max f) - (max f) by XREAL_1:9, RFINSEQ2:1;
hence r <= 0 by A2, A3; :: thesis: verum

end;

hence f - (max f) is nonpositive-yielding by PARTFUN3:def 3; :: thesis: verum