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

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