( dom p = X & rng p = X & dom M = X ) by FUNCT_2:def 3, PARTFUN1:def 2;
then dom (M * p) = X by RELAT_1:27;
hence M * p is total by PARTFUN1:def 2; :: thesis: verum