set
F
=
sqrt
f
;
(
dom
(
sqrt
f
)
=
dom
f
&
rng
(
sqrt
f
)
c=
REAL
)
by
Def5
,
VALUED_0:def 3
;
hence
sqrt
f
is
PartFunc
of
C
,
REAL
by
RELSET_1:4
;
:: thesis:
verum