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