let C be Cartesian_category; :: thesis: for a, b being Object of C st Hom a,b <> {} & Hom b,a <> {} holds
( pr1 a,b is retraction & pr2 a,b is retraction )
let a, b be Object of C; :: thesis: ( Hom a,b <> {} & Hom b,a <> {} implies ( pr1 a,b is retraction & pr2 a,b is retraction ) )
A1: cod (pr2 a,b) = b by Def9;
( a [x] b is_a_product_wrt pr1 a,b, pr2 a,b & cod (pr1 a,b) = a ) by Def9;
hence ( Hom a,b <> {} & Hom b,a <> {} implies ( pr1 a,b is retraction & pr2 a,b is retraction ) ) by A1, CAT_3:62; :: thesis: verum