defpred S1[ 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 S1[i,j]
let i be object ; :: thesis: ( i in I implies ex j being object st S1[i,j] )
assume i in I ; :: thesis: ex j being object st S1[i,j]
defpred S2[ 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 & S2[x] ) ) from reconsider j = j as object ;
take j = j; :: thesis: S1[i,j]
thus S1[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
S1[i,A . i] from 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
S1[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 S1[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 ;
S1[i,A . i] by A3, A6;
hence x in A . i by A7, A8, A9; :: thesis: verum
end;