reconsider f = {} as Function ;
reconsider f = f as PartFunc of X,REAL by RELSET_1:25;
take f ; :: thesis: f is nonnegative
let x be Element of ExtREAL ; :: according to SUPINF_2:def 15,SUPINF_2:def 22 :: thesis: ( not x in rng f or K389() <= x )
thus ( not x in rng f or K389() <= x ) ; :: thesis: verum