let Ch be Choice of M; :: thesis: Ch is ManySortedSet of I
dom Ch = dom M by Def1
.= I by PARTFUN1:def 2 ;
then Ch is I -defined total Function by RELAT_1:def 18, PARTFUN1:def 2;
hence Ch is ManySortedSet of I ; :: thesis: verum