let X, Y be ManySortedSet of I; :: thesis: ( ( for i being object st i in I holds
X . i = (F . i) " (A . i) ) & ( for i being object st i in I holds
Y . i = (F . i) " (A . i) ) implies X = Y )
assume that
A1: for i being object st i in I holds
X . i = (F . i) " (A . i) and
A2: for i being object st i in I holds
Y . i = (F . i) " (A . i) ; :: thesis: X = Y

now :: thesis: for i being object st i in I holds
X . i = Y . i

let i be object ; :: thesis: ( i in I implies X . i = Y . i )
assume A3: i in I ; :: thesis: X . i = Y . i
hence X . i = (F . i) " (A . i) by A1
.= Y . i by A2, A3 ;
:: thesis: verum

end;

hence X = Y ; :: thesis: verum