reconsider f = {} as Function ;
reconsider f = f as PartFunc of X,REAL by RELSET_1:12;
take f ; :: thesis: f is nonnegative
let x be ExtReal; :: according to SUPINF_2:def 9,SUPINF_2:def 11 :: thesis: ( not x in rng f or 0. <= x )
thus ( not x in rng f or 0. <= x ) ; :: thesis: verum