theorem :: ALTCAT_6: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 & Union (coprod A) = {} holds
EnsCatCoproduct A = I --> {}