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

A1: now

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
assume i in I ; :: thesis: ex j being set st S₁[i,j]
defpred S₂[ set ] 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 set holds
( x in j iff ( x in M . i & S₂[x] ) ) from XBOOLE_0:sch 1();
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 set st i in I holds
S₁[i,A . i] from PBOOLE:sch 3(A1);
A is ManySortedSubset of M

proof

let i be set ; :: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in M . i )
assume x in A . i ; :: thesis: x in M . i
hence x in M . i by A3, A4; :: thesis: verum

end;

then reconsider A = A as ManySortedSubset of M ;
take A ; :: thesis: for x, i being set 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, i being set 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, i be set ; :: 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 A5: i in I ; :: thesis: ( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) )
hence ( x in A . i implies ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) by A3; :: 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 A6: f = F . i and
A7: ( x in dom f & f . x = x ) ; :: thesis: x in A . i
doms F = M by MSSUBFAM:17;
then dom f = M . i by A5, A6, MSSUBFAM:14;
hence x in A . i by A3, A5, A6, A7; :: thesis: verum

end;