:: deftheorem Def10 defines EnsCatProductObj ALTCAT_5:def 10 :
for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st product A in E holds
EnsCatProductObj A = product A;