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: ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19;
( a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) & cod (pr1 (a,b)) = a ) by Def8;
hence ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( pr1 (a,b) is retraction & pr2 (a,b) is retraction ) ) by A1, CAT_3:57; :: thesis: verum