let C be Category; :: thesis: for c being Object of C
for h, p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 holds
h = id c
let c be Object of C; :: thesis: for h, p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 holds
h = id c
let h, p1, p2 be Morphism of C; :: thesis: ( c is_a_product_wrt p1,p2 & h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 implies h = id c )
assume that
A1: ( dom p1 = c & dom p2 = c ) and
A2: for d being Object of C
for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds
ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) and
A3: ( h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 ) ; :: according to CAT_3:def 15 :: thesis: h = id c
( p1 in Hom (c,(cod p1)) & p2 in Hom (c,(cod p2)) ) by A1;
then consider i being Morphism of C such that
i in Hom (c,c) and
A4: for k being Morphism of C st k in Hom (c,c) holds
( ( p1 (*) k = p1 & p2 (*) k = p2 ) iff i = k ) by A2;
A5: id c in Hom (c,c) by CAT_1:27;
( p1 (*) (id c) = p1 & p2 (*) (id c) = p2 ) by A1, CAT_1:22;
hence id c = i by A4, A5
.= h by A3, A4 ;
:: thesis: verum