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