let C be Category; :: thesis: for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & Hom ((cod p1),(cod p2)) <> {} & Hom ((cod p2),(cod p1)) <> {} holds
( p1 is retraction & p2 is retraction )
let c be Object of C; :: thesis: for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & Hom ((cod p1),(cod p2)) <> {} & Hom ((cod p2),(cod p1)) <> {} holds
( p1 is retraction & p2 is retraction )
let p1, p2 be Morphism of C; :: thesis: ( c is_a_product_wrt p1,p2 & Hom ((cod p1),(cod p2)) <> {} & Hom ((cod p2),(cod p1)) <> {} implies ( p1 is retraction & p2 is retraction ) )
assume that
A1: c is_a_product_wrt p1,p2 and
A2: ( Hom ((cod p1),(cod p2)) <> {} & Hom ((cod p2),(cod p1)) <> {} ) ; :: thesis: ( p1 is retraction & p2 is retraction )
set I = {0,1};
set F = (0,1) --> (p1,p2);
A3: ((0,1) --> (p1,p2)) /. 0 = p1 by Th7;

A4: now

( dom p1 = c & dom p2 = c ) by A1, Def16;
hence (0,1) --> (p1,p2) is Projections_family of c,{0,1} by Th48; :: thesis: ( c is_a_product_wrt (0,1) --> (p1,p2) & ( for x1, x2 being set st x1 in {0,1} & x2 in {0,1} holds
Hom ((cod (((0,1) --> (p1,p2)) /. x1)),(cod (((0,1) --> (p1,p2)) /. x2))) <> {} ) )
thus c is_a_product_wrt (0,1) --> (p1,p2) by A1, Th59; :: thesis: for x1, x2 being set st x1 in {0,1} & x2 in {0,1} holds
Hom ((cod (((0,1) --> (p1,p2)) /. x1)),(cod (((0,1) --> (p1,p2)) /. x2))) <> {}
let x1, x2 be set ; :: thesis: ( x1 in {0,1} & x2 in {0,1} implies Hom ((cod (((0,1) --> (p1,p2)) /. x1)),(cod (((0,1) --> (p1,p2)) /. x2))) <> {} )
assume that
A5: x1 in {0,1} and
A6: x2 in {0,1} ; :: thesis: Hom ((cod (((0,1) --> (p1,p2)) /. x1)),(cod (((0,1) --> (p1,p2)) /. x2))) <> {}
A7: ( x2 = 0 or x2 = 1 ) by A6, TARSKI:def 2;
( x1 = 0 or x1 = 1 ) by A5, TARSKI:def 2;
hence Hom ((cod (((0,1) --> (p1,p2)) /. x1)),(cod (((0,1) --> (p1,p2)) /. x2))) <> {} by A2, A3, A7, Th7, CAT_1:56; :: thesis: verum

end;

A8: 1 in {0,1} by TARSKI:def 2;
( ((0,1) --> (p1,p2)) /. 1 = p2 & 0 in {0,1} ) by Th7, TARSKI:def 2;
hence ( p1 is retraction & p2 is retraction ) by A3, A4, A8, Th54; :: thesis: verum