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