theorem :: CAT_3:57

for C being Category
for a, b, c being Object of C
for p1 being Morphism of c,a
for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( p1 is retraction & p2 is retraction )