let N1, N2 be ManySortedSet of I * ; :: thesis: ( ( for i being Element of I * holds N1 . i = product (M * i) ) & ( for i being Element of I * holds N2 . i = product (M * i) ) implies N1 = N2 )
assume that
A3: for i being Element of I * holds N1 . i = product (M * i) and
A4: for i being Element of I * holds N2 . i = product (M * i) ; :: thesis: N1 = N2

now :: thesis: for i being object st i in I * holds
N1 . i = N2 . i

let i be object ; :: thesis: ( i in I * implies N1 . i = N2 . i )
assume i in I * ; :: thesis: N1 . i = N2 . i
then reconsider e = i as Element of I * ;
thus N1 . i = product (M * e) by A3
.= N2 . i by A4 ; :: thesis: verum

end;

hence N1 = N2 ; :: thesis: verum