A1
: the
carrier
of
(
R^1

(
R^1
(
rng
f
)
)
)
=
R^1
(
rng
f
)
by
PRE_TOPC:8
;
the
carrier
of
(
R^1

(
R^1
(
dom
f
)
)
)
=
R^1
(
dom
f
)
by
PRE_TOPC:8
;
hence
f
is
Function
of
(
R^1

(
R^1
(
dom
f
)
)
)
,
(
R^1

(
R^1
(
rng
f
)
)
)
by
A1
,
FUNCT_2:2
;
:: thesis:
verum