let X, Y be ManySortedSet of ; :: thesis: ( ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & X . j = the carrier of R ) ) & ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & Y . j = the carrier of R ) ) implies X = Y )
assume that
A5: for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & X . j = the carrier of R ) and
A6: for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & Y . j = the carrier of R ) ; :: thesis: X = Y
for i being set st i in J holds
X . i = Y . i

proof

let i be set ; :: thesis: ( i in J implies X . i = Y . i )
assume i in J ; :: thesis: X . i = Y . i
then ( ex R being 1-sorted st
( R = A . i & X . i = the carrier of R ) & ex R being 1-sorted st
( R = A . i & Y . i = the carrier of R ) ) by A5, A6;
hence X . i = Y . i ; :: thesis: verum

end;

hence X = Y by PBOOLE:3; :: thesis: verum