let
f
be
PartFunc
of
REAL
,
REAL
;
:: thesis:
(
dom
f
=
REAL
implies
R^1

(
R^1
(
dom
f
)
)
=
R^1
)
assume
dom
f
=
REAL
;
:: thesis:
R^1

(
R^1
(
dom
f
)
)
=
R^1
then
[#]
R^1
=
R^1
(
dom
f
)
by
TOPMETR:17
;
hence
R^1

(
R^1
(
dom
f
)
)
=
R^1
by
PRE_TOPC:def 5
;
:: thesis:
verum