let I be set ; :: according to ALTCAT_6:def 7 :: thesis: for A being ObjectsFamily of I,(EnsCat {{}}) ex B being Object of (EnsCat {{}}) ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms )
let A be ObjectsFamily of I,(EnsCat {{}}); :: thesis: ex B being Object of (EnsCat {{}}) ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms )
reconsider o = {} as Object of (EnsCat {{}}) by Lm1, TARSKI:def 1;
reconsider P = I --> {} as MorphismsFamily of A,o by Th3;
take o ; :: thesis: ex P being MorphismsFamily of A,o st
( P is feasible & P is coprojection-morphisms )
take P ; :: thesis: ( P is feasible & P is coprojection-morphisms )
thus ( P is feasible & P is coprojection-morphisms ) by Th4; :: thesis: verum