H0
: the
carrier
of
(
RenField
r
)
=
rng
r
by
defrf
.=
dom
(
r
"
)
by
FUNCT_1:33
;
rng
(
r
"
)
=
dom
r
by
FUNCT_1:33
.= the
carrier
of
F
by
defr
;
hence
r
"
is
Function
of
(
RenField
r
)
,
F
by
H0
,
FUNCT_2:1
;
:: thesis:
verum