let
f
be
Function
of
REAL
,
REAL
;
:: thesis:
f
is
Function
of
R^1
,
R^1
dom
f
=
REAL
by
FUNCT_2:def 1
;
then
reconsider
B
=
rng
f
as non
empty
Subset
of
REAL
by
RELAT_1:42
;
f
is
Function
of
R^1
,
(
R^1

(
R^1
B
)
)
by
Th7
;
hence
f
is
Function
of
R^1
,
R^1
by
TOPREALA:7
;
:: thesis:
verum