reconsider F1 = F1, F2 = F2 as PartFunc of D,E ;
F1 + F2 is PartFunc of D,COMPLEX ;
hence F1 + F2 is Element of PFuncs (D,COMPLEX) by PARTFUN1:45; :: thesis: verum