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