let A, B be ManySortedSubset of M; :: 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 ) ) ) & ( for x being set
for i being object 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
A10: 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 ) ) and
A11: for x being set
for i being object 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 :: thesis: for i being object st i in I holds
A . i = B . i

let i be object ; :: thesis: ( i in I implies A . i = B . i )
assume A12: 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 object ; :: 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 A10, A12;
hence x in B . i by A11, A12; :: thesis: verum

end;

let x be object ; :: 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 A11, A12;
hence x in A . i by A10, A12; :: thesis: verum

end;

end;

hence A = B ; :: thesis: verum