let I be set ; :: thesis: for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds
EnsCatCoproductObj A is A -CatCoproduct-like
let E be non empty set ; :: thesis: for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds
EnsCatCoproductObj A is A -CatCoproduct-like
let A be ObjectsFamily of I,(EnsCat E); :: thesis: ( Union (coprod A) in E implies EnsCatCoproductObj A is A -CatCoproduct-like )
assume A1: Union (coprod A) in E ; :: thesis: EnsCatCoproductObj A is A -CatCoproduct-like
take EnsCatCoproduct A ; :: according to ALTCAT_6:def 8 :: thesis: ( EnsCatCoproduct A is feasible & EnsCatCoproduct A is coprojection-morphisms )
thus ( EnsCatCoproduct A is feasible & EnsCatCoproduct A is coprojection-morphisms ) by A1, Th10; :: thesis: verum