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

proof

let x be object ; :: 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 ; :: thesis: verum