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