consider F being Function of NAT,ExtREAL;
reconsider A = rng F as non empty Subset of ExtREAL ;
take A ; :: thesis: A is countable
assume not A is empty ; :: according to SUPINF_2:def 14 :: 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