theorem Th33: :: SUPINF_2:34

( 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 )