NAT c= ExtREAL by NUMBERS:19, NUMBERS:31;
then reconsider F = id NAT as sequence of ExtREAL by FUNCT_2:7;
rng F c= ExtREAL ;
hence ( id NAT is sequence of ExtREAL & id NAT is one-to-one & NAT = rng (id NAT) & rng (id NAT) is non empty Subset of ExtREAL ) ; :: thesis: verum