:: deftheorem Def11 defines EnsCatProduct ALTCAT_5:def 11 :
for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st product A in E holds
for b₄ being MorphismsFamily of EnsCatProductObj A,A holds
( b₄ = EnsCatProduct A iff for i being set st i in I holds
b₄ . i = proj (A,i) );