dom (Mphs F) = dom F by Def3
.= A by PARTFUN1:def 4 ;
hence Mphs F is V2() ManySortedSet of A by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum