theorem Th7: :: WAYBEL18:7

for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds
product J is injective