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