reconsider F = F as PartFunc of D,E ;
F ^ is PartFunc of D, REAL ;
hence F ^ is Element of PFuncs D,REAL by PARTFUN1:119; :: thesis: verum