dom (Mphs F) = dom F by Def3
.= A by PARTFUN1:def 2 ;
hence Mphs F is total by PARTFUN1:def 2; :: thesis: verum