let A1, A2 be ManySortedSet of I; ( ( for i being object st i in I holds
A1 . i = (X . i) /\ (Y . i) ) & ( for i being object st i in I holds
A2 . i = (X . i) /\ (Y . i) ) implies A1 = A2 )
assume that
A8:
for i being object st i in I holds
A1 . i = (X . i) /\ (Y . i)
and
A9:
for i being object st i in I holds
A2 . i = (X . i) /\ (Y . i)
; A1 = A2
hence
A1 = A2
by Th3; verum