for I being non empty set
for X, Y being ManySortedSet of I
for i being Element of I * holds product ((X (/\) Y) * i) = (product (X * i)) /\ (product (Y * i))