let C be Cartesian_category; :: thesis: for a, b being Object of C holds
( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a )
let a, b be Object of C; :: thesis: ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a )
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 Def8;
hence ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) by Def8; :: thesis: verum