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