let C be Cartesian_category; :: thesis: for a, b being Object of C holds
( dom (pr2 a,b) = a [x] b & cod (pr2 a,b) = b )
let a, b be Object of C; :: thesis: ( dom (pr2 a,b) = a [x] b & cod (pr2 a,b) = b )
set p1 = the Proj1 of C . a,b;
set p2 = the Proj2 of C . a,b;
a [x] b is_a_product_wrt the Proj1 of C . a,b,the Proj2 of C . a,b by Def9;
hence ( dom (pr2 a,b) = a [x] b & cod (pr2 a,b) = b ) by Def9, CAT_3:def 16; :: thesis: verum