dom
r
=
X
by
defr
;
then
r
is
Function
of
X
,
(
rng
r
)
by
FUNCT_2:2
;
hence
r
"
is
Function
of
(
rng
r
)
,
X
by
FUNCT_2:25
;
:: thesis:
verum