defpred S₁[ object , object ] means ex a being Element of M . I st M = {a};

A1: now :: thesis: for i being object st i in I holds
ex j being object st S₁[i,j]

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume i in I ; :: thesis: ex j being object st S₁[i,j]
set a = the Element of M . i;
reconsider j = { the Element of M . i} as object ;
take j = j; :: thesis: S₁[i,j]
thus S₁[i,j] ; :: thesis: verum

end;

consider C being ManySortedSet of I such that
A2: for i being object st i in I holds
S₁[i,C . i] from PBOOLE:sch 3(A1);
C is ManySortedSubset of M

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in I or C . i c= M . i )
assume A3: i in I ; :: thesis: C . i c= M . i
then A4: not M . i is empty ;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in C . i or q in M . i )
consider a being Element of M . i such that
A5: C . i = {a} by A2, A3;
assume q in C . i ; :: thesis: q in M . i
then q = a by A5, TARSKI:def 1;
hence q in M . i by A4; :: thesis: verum

end;

then reconsider C = C as ManySortedSubset of M ;
take C ; :: thesis: ( C is non-empty & C is finite-yielding )
thus C is non-empty :: thesis: C is finite-yielding

proof

let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not C . i is empty )
assume i in I ; :: thesis: not C . i is empty
then ex a being Element of M . i st C . i = {a} by A2;
hence not C . i is empty ; :: thesis: verum

end;

let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or C . i is finite )
assume i in I ; :: thesis: C . i is finite
then ex a being Element of M . i st C . i = {a} by A2;
hence C . i is finite ; :: thesis: verum