for X being non empty 1-sorted
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj (J,i)) * f