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 Def8;
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) ) ;
( cod ( the Proj1 of C . (a,b)) = a & cod ( the Proj2 of C . (a,b)) = b ) by Def8;
hence ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by A1, CAT_1:1; :: thesis: verum