let f, g be ManySortedSet of ; :: 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 x in I ; :: thesis: f . x = g . x
then ( f . x = [:(X . x),(Y . x):] & g . x = [:(X . x),(Y . x):] ) by A2, A3;
hence f . x = g . x ; :: thesis: verum

end;

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