theorem Th7: :: ALTCAT_5:7

for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st product A in E & product A = {} holds
EnsCatProduct A = I --> {}