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