theorem :: YELLOW17:23

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 compact ) holds
product J is compact