defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & ( for x being object holds
( x in D2 iff ( x in M . $1 & ex f being Function st
( f = F . $1 & x in dom f & f . x = x ) ) ) ) );

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]
defpred S₂[ object ] means ex f being Function st
( f = F . i & $1 in dom f & f . $1 = $1 );
consider j being set such that
A2: for x being object holds
( x in j iff ( x in M . i & S₂[x] ) ) from XBOOLE_0:sch 1();
reconsider j = j as object ;
take j = j; :: thesis: S₁[i,j]
thus S₁[i,j] by A2; :: thesis: verum

end;

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

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in I or A . i c= M . i )
assume A4: i in I ; :: thesis: A . i c= M . i
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in M . i )
assume A5: x in A . i ; :: thesis: x in M . i
S₁[i,A . i] by A3, A4;
hence x in M . i by A5; :: thesis: verum

end;

then reconsider A = A as ManySortedSubset of M ;
take A ; :: thesis: for x being set
for i being object st i in I holds
( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) )
thus for x being set
for i being object st i in I holds
( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) :: thesis: verum

proof

let x be set ; :: thesis: for i being object st i in I holds
( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) )
let i be object ; :: thesis: ( i in I implies ( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) )
assume A6: i in I ; :: thesis: ( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) )
then S₁[i,A . i] by A3;
hence ( x in A . i implies ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ; :: thesis: ( ex f being Function st
( f = F . i & x in dom f & f . x = x ) implies x in A . i )
given f being Function such that A7: f = F . i and
A8: ( x in dom f & f . x = x ) ; :: thesis: x in A . i
doms F = M by MSSUBFAM:17;
then A9: dom f = M . i by A6, A7, MSSUBFAM:14;
S₁[i,A . i] by A3, A6;
hence x in A . i by A7, A8, A9; :: thesis: verum

end;