defpred S_{1}[ 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 ) ) ) ) );

A3: for i being object st i in I holds

S_{1}[i,A . i]
from PBOOLE:sch 3(A1);

A is 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

( 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_{1}[i,j]

consider A being ManySortedSet of I such that ex j being object st S

let i be object ; :: thesis: ( i in I implies ex j being object st S_{1}[i,j] )

assume i in I ; :: thesis: ex j being object st S_{1}[i,j]

defpred S_{2}[ 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_{2}[x] ) )
from XBOOLE_0:sch 1();

reconsider j = j as object ;

take j = j; :: thesis: S_{1}[i,j]

thus S_{1}[i,j]
by A2; :: thesis: verum

end;assume i in I ; :: thesis: ex j being object st S

defpred S

( 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

reconsider j = j as object ;

take j = j; :: thesis: S

thus S

A3: for i being object st i in I holds

S

A is ManySortedSubset of M

proof

then reconsider A = A as ManySortedSubset of M ;
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_{1}[i,A . i]
by A3, A4;

hence x in M . i by A5; :: thesis: verum

end;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

hence x in M . i by A5; :: thesis: verum

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_{1}[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_{1}[i,A . i]
by A3, A6;

hence x in A . i by A7, A8, A9; :: thesis: verum

end;( 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

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

hence x in A . i by A7, A8, A9; :: thesis: verum