let E be non empty set ; :: thesis: ( ( for I being set
for A being ObjectsFamily of I,(EnsCat E) holds Union (coprod A) in E ) implies EnsCat E is with_coproducts )
assume A1: for I being set
for A being ObjectsFamily of I,(EnsCat E) holds Union (coprod A) in E ; :: thesis: EnsCat E is with_coproducts
let I be set ; :: according to ALTCAT_6:def 7 :: thesis: for A being ObjectsFamily of I,(EnsCat E) ex B being Object of (EnsCat E) ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms )
let A be ObjectsFamily of I,(EnsCat E); :: thesis: ex B being Object of (EnsCat E) ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms )
take EnsCatCoproductObj A ; :: thesis: ex P being MorphismsFamily of A, EnsCatCoproductObj A st
( P is feasible & P is coprojection-morphisms )
take EnsCatCoproduct A ; :: thesis: ( EnsCatCoproduct A is feasible & EnsCatCoproduct A is coprojection-morphisms )
Union (coprod A) in E by A1;
hence ( EnsCatCoproduct A is feasible & EnsCatCoproduct A is coprojection-morphisms ) by Th10; :: thesis: verum