let X, Y be ManySortedSet of ; :: thesis: ( ( for i being set st i in I holds
X . i = {} (A . i) ) & ( for i being set st i in I holds
Y . i = {} (A . i) ) implies X = Y )
assume A2: ( ( for i being set st i in I holds
X . i = {} (A . i) ) & ( for i being set st i in I holds
Y . i = {} (A . i) ) ) ; :: thesis: X = Y
for i being set st i in I holds
X . i = Y . i

proof

let i be set ; :: thesis: ( i in I implies X . i = Y . i )
assume i in I ; :: thesis: X . i = Y . i
then ( X . i = {} (A . i) & Y . i = {} (A . i) ) by A2;
hence X . i = Y . i ; :: thesis: verum

end;

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