theorem Th1: :: MSAFREE:1

for I being set
for J being non empty set
for f being Function of I,(J *)
for X being ManySortedSet of J
for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)