set F = the Function of NAT,ExtREAL;
reconsider A = rng the Function of NAT,ExtREAL as non empty Subset of ExtREAL ;
take A ; :: thesis: A is countable
assume not A is empty ; :: according to SUPINF_2:def 8 :: thesis: ex F being Function of NAT,ExtREAL st A = rng F
thus ex F being Function of NAT,ExtREAL st A = rng F ; :: thesis: verum