dom (coprod ) = dom X
by CARD_3:def 3;

then dom (coprod ) = I by PARTFUN1:def 2;

hence coprod is I -defined by RELAT_1:def 18; :: thesis: verum

then dom (coprod ) = I by PARTFUN1:def 2;

hence coprod is I -defined by RELAT_1:def 18; :: thesis: verum