let A1, A2 be ManySortedSet of ; :: 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
A3: for i being set st i in I holds
A1 . i = (X . i) \/ (Y . i) and
A4: 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 A5: i in I ; :: thesis: A1 . i = A2 . i
hence A1 . i = (X . i) \/ (Y . i) by A3
.= A2 . i by A4, A5 ;
:: thesis: verum

end;

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