for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for f being Element of (product J) holds (proj (J,i)) . f = f . i