let
f
be
Function
of
REAL
,
REAL
;
:: thesis:
f
is
Function
of
R^1
,
(
R^1

(
R^1
(
rng
f
)
)
)
REAL
=
dom
f
by
FUNCT_2:def 1
;
then
R^1

(
R^1
(
dom
f
)
)
=
R^1
by
Th6
;
then
R^1
f
is
Function
of
R^1
,
(
R^1

(
R^1
(
rng
f
)
)
)
;
hence
f
is
Function
of
R^1
,
(
R^1

(
R^1
(
rng
f
)
)
)
;
:: thesis:
verum