let C be category; :: thesis: for A being ObjectsFamily of {},C
for B being Object of C st B is terminal holds
B is A -CatProduct-like
let A be ObjectsFamily of {},C; :: thesis: for B being Object of C st B is terminal holds
B is A -CatProduct-like
let B be Object of C; :: thesis: ( B is terminal implies B is A -CatProduct-like )
assume B is terminal ; :: thesis: B is A -CatProduct-like
then ex P being MorphismsFamily of B,A st
( P is empty & P is projection-morphisms ) by Th2;
hence B is A -CatProduct-like ; :: thesis: verum