let A, B be ManySortedSubset of M; :: 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 ) ) ) & ( for x, i being set st i in I holds
( x in B . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ) implies A = B )
assume that
A8: 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 ) ) and
A9: for x, i being set st i in I holds
( x in B . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ; :: thesis: A = B

now

let i be set ; :: thesis: ( i in I implies A . i = B . i )
assume A10: i in I ; :: thesis: A . i = B . i
thus A . i = B . i :: thesis: verum

proof

thus A . i c= B . i :: according to XBOOLE_0:def 10 :: thesis: B . i c= A . i

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in B . i )
assume x in A . i ; :: thesis: x in B . i
then ex f being Function st
( f = F . i & x in dom f & f . x = x ) by A8, A10;
hence x in B . i by A9, A10; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B . i or x in A . i )
assume x in B . i ; :: thesis: x in A . i
then ex f being Function st
( f = F . i & x in dom f & f . x = x ) by A9, A10;
hence x in A . i by A8, A10; :: thesis: verum

end;

end;

hence A = B by PBOOLE:3; :: thesis: verum