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