dom (coprod ) = dom X by CARD_3:def 3;
then dom (coprod ) = I by PARTFUN1:def 4;
hence coprod is total by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum