let C be Cartesian_category; 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; ( 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; verum