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