dom
(
sqrt
f
)
=
dom
f
by
Def5
.=
X
by
FUNCT_2:def 1
;
hence
sqrt
f
is
Function
of
X
,
REAL
by
FUNCT_2:def 1
;
:: thesis:
verum