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