let I be set ; :: thesis: for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st product A in E holds
EnsCatProductObj A is A -CatProduct-like
let E be non empty set ; :: thesis: for A being ObjectsFamily of I,(EnsCat E) st product A in E holds
EnsCatProductObj A is A -CatProduct-like
let A be ObjectsFamily of I,(EnsCat E); :: thesis: ( product A in E implies EnsCatProductObj A is A -CatProduct-like )
assume A1: product A in E ; :: thesis: EnsCatProductObj A is A -CatProduct-like
take EnsCatProduct A ; :: according to ALTCAT_5:def 9 :: thesis: ( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )
thus ( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms ) by A1, Th8; :: thesis: verum