dom
(
f
^
)
=
dom
f
by
Th2
.=
X
by
FUNCT_2:def 1
;
hence
f
^
is
Function
of
X
,
REAL
by
FUNCT_2:def 1
;
:: thesis:
verum