for r being Real st r in rng (f - (min f)) holds
r >= 0

proof

let r be Real; :: thesis: ( r in rng (f - (min f)) implies r >= 0 )
assume A1: r in rng (f - (min f)) ; :: thesis: r >= 0
consider x being object such that
A2: ( x in dom (f - (min f)) & r = (f - (min f)) . x ) by A1, FUNCT_1:def 3;
A3: ( dom (f - (min f)) = dom f & ( for i being object st i in dom f holds
(f - (min f)) . i = (f . i) - (min 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) - (min f) >= (min f) - (min f) by XREAL_1:9, RFINSEQ2:2;
hence r >= 0 by A2, A3; :: thesis: verum

end;

hence f - (min f) is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum