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
A13: for i being set st i in I holds
A1 . i = (X . i) \ (Y . i) and
A14: 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 A15: i in I ; :: thesis: A1 . i = A2 . i
hence A1 . i = (X . i) \ (Y . i) by A13
.= A2 . i by A14, A15 ;
:: thesis: verum

end;

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