let C be Cartesian_category; :: thesis: for a, b being Object of C holds
( Hom (a [x] b),a <> {} & Hom (a [x] b),b <> {} )
let a, b be Object of C; :: thesis: ( Hom (a [x] b),a <> {} & Hom (a [x] b),b <> {} )
set c = the CatProd of C . a,b;
set p1 = the Proj1 of C . a,b;
set p2 = the Proj2 of C . a,b;
the CatProd of C . a,b is_a_product_wrt the Proj1 of C . a,b,the Proj2 of C . a,b by Def9;
then A1: ( dom (the Proj1 of C . a,b) = the CatProd of C . a,b & dom (the Proj2 of C . a,b) = the CatProd of C . a,b ) by CAT_3:def 16;
( cod (the Proj1 of C . a,b) = a & cod (the Proj2 of C . a,b) = b ) by Def9;
hence ( Hom (a [x] b),a <> {} & Hom (a [x] b),b <> {} ) by A1, CAT_1:18; :: thesis: verum