( dom f1 = dom f & dom f2 = dom f ) by PARTFUN1:def 2;
hence f1 + f2 = f1 ; :: thesis: verum