let E be non empty set ; :: thesis: ( ( for I being set
for A being ObjectsFamily of I,(EnsCat E) holds product A in E ) implies EnsCat E is with_products )
assume A1: for I being set
for A being ObjectsFamily of I,(EnsCat E) holds product A in E ; :: thesis: EnsCat E is with_products
let I be set ; :: according to ALTCAT_5:def 8 :: thesis: for A being ObjectsFamily of I,(EnsCat E) ex B being Object of (EnsCat E) ex P being MorphismsFamily of B,A st
( P is feasible & P is projection-morphisms )
let A be ObjectsFamily of I,(EnsCat E); :: thesis: ex B being Object of (EnsCat E) ex P being MorphismsFamily of B,A st
( P is feasible & P is projection-morphisms )
take EnsCatProductObj A ; :: thesis: ex P being MorphismsFamily of EnsCatProductObj A,A st
( P is feasible & P is projection-morphisms )
take EnsCatProduct A ; :: thesis: ( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )
product A in E by A1;
hence ( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms ) by Th8; :: thesis: verum