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