let Ch be ManySortedSet of I; :: thesis: ( Ch is Choice of M iff for x being object st x in I holds
Ch . x = the Element of M . x )
dom M = I by PARTFUN1:def 2;
hence ( Ch is Choice of M implies for x being object st x in I holds
Ch . x = the Element of M . x ) by Def1; :: thesis: ( ( for x being object st x in I holds
Ch . x = the Element of M . x ) implies Ch is Choice of M )
assume A1: for x being object st x in I holds
Ch . x = the Element of M . x ; :: thesis: Ch is Choice of M
thus dom Ch = I by PARTFUN1:def 2
.= dom M by PARTFUN1:def 2 ; :: according to ORDERS_1:def 1 :: thesis: for x being object st x in dom M holds
Ch . x = the Element of M . x
thus for x being object st x in dom M holds
Ch . x = the Element of M . x by A1; :: thesis: verum