let f, g be ManySortedSet of I; :: thesis: ( ( for i being set st i in I holds
f . i = [:(X . i),(Y . i):] ) & ( for i being set st i in I holds
g . i = [:(X . i),(Y . i):] ) implies f = g )
assume that
A2: for i being set st i in I holds
f . i = [:(X . i),(Y . i):] and
A3: for i being set st i in I holds
g . i = [:(X . i),(Y . i):] ; :: thesis: f = g
for x being set st x in I holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in I implies f . x = g . x )
assume A4: x in I ; :: thesis: f . x = g . x
then f . x = [:(X . x),(Y . x):] by A2;
hence f . x = g . x by A3, A4; :: thesis: verum

end;

hence f = g by Th3; :: thesis: verum