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