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