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

now

let i be set ; :: thesis: ( i in I implies A1 . i = A2 . i )
assume A10: i in I ; :: thesis: A1 . i = A2 . i
hence A1 . i = (X . i) /\ (Y . i) by A8
.= A2 . i by A9, A10 ;
:: thesis: verum

end;

hence A1 = A2 by Th3; :: thesis: verum