( dom g = X & dom f c= X ) by PARTFUN1:def 2;
hence f +* g = g null f by FUNCT_4:19; :: thesis: verum