theorem :: ALTCAT_6:12

for E being non empty set st ( for I being set
for A being ObjectsFamily of I,(EnsCat E) holds Union (coprod A) in E ) holds
EnsCat E is with_coproducts