reconsider F1 = F1, F2 = F2 as PartFunc of , ;
F1 + F2 is PartFunc of , ;
hence F1 + F2 is Element of PFuncs D,REAL by PARTFUN1:119; :: thesis: verum