:: deftheorem Def9 defines EnsCatCoproductObj ALTCAT_6:def 9 :
for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds
EnsCatCoproductObj A = Union (coprod A);