reconsider F = incl NAT as Function of NAT,ExtREAL by FUNCT_2:7, NUMBERS:31;
rng F c= ExtREAL ;
hence ( incl NAT is Function of NAT,ExtREAL & incl NAT is one-to-one & NAT = rng (incl NAT) & rng (incl NAT) is non empty Subset of ExtREAL ) by RELAT_1:45; :: thesis: verum