A1: dom (f1 + f2) = (dom f1) /\ (dom f2) by Def1;
( dom f1 = X & dom f2 = X ) by PARTFUN1:def 2;
hence f1 + f2 is total by A1, PARTFUN1:def 2; :: thesis: verum