dom
f
=
X
by
FUNCT_2:def 1
;
then
A1
:
dom
|[
f
]|
=
X
by
Def1
;
rng
|[
f
]|
c=
the
carrier
of
(
TOP-REAL
1
)
;
hence
|[
f
]|
is
Function
of
X
,
(
TOP-REAL
1
)
by
A1
,
FUNCT_2:2
;
:: thesis:
verum