dom (f +* g) = (dom f) \/ (dom g) by Def1;
then dom (f +* g) c= I ;
hence f +* g is I -defined by RELAT_1:def 18; :: thesis: verum