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 & cod p2 is terminal holds
c, cod p1 are_isomorphic
let c be Object of C; :: thesis: for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p2 is terminal holds
c, cod p1 are_isomorphic
let p1, p2 be Morphism of C; :: thesis: ( c is_a_product_wrt p1,p2 & cod p2 is terminal implies c, cod p1 are_isomorphic )
set a = cod p1;
set b = cod p2;
assume that
A1: c is_a_product_wrt p1,p2 and
A2: cod p2 is terminal ; :: thesis: c, cod p1 are_isomorphic
set f = id (cod p1);
set g = term (cod p1),(cod p2);
( dom (term (cod p1),(cod p2)) = cod p1 & cod (term (cod p1),(cod p2)) = cod p2 ) by A2, Th39;
then ( id (cod p1) in Hom (cod p1),(cod p1) & term (cod p1),(cod p2) in Hom (cod p1),(cod p2) ) by CAT_1:55;
then consider h being Morphism of C such that
A3: h in Hom (cod p1),c and
A4: for k being Morphism of C st k in Hom (cod p1),c holds
( ( p1 * k = id (cod p1) & p2 * k = term (cod p1),(cod p2) ) iff h = k ) by A1, Def16;
A5: dom h = cod p1 by A3, CAT_1:18;
A6: dom p1 = c by A1, Def16;
then reconsider p = p1 as Morphism of c, cod p1 by CAT_1:22;
A7: cod h = c by A3, CAT_1:18;
then A8: cod (h * p) = c by A5, CAT_1:42;
A9: dom p2 = c by A1, Def16;
then A10: cod (p2 * (h * p)) = cod p2 by A8, CAT_1:42;
A11: dom (h * p) = c by A6, A5, CAT_1:42;
then A12: h * p in Hom c,c by A8;
dom (p2 * (h * p)) = c by A9, A11, A8, CAT_1:42;
then A13: p2 * (h * p) = term c,(cod p2) by A2, A10, Th40
.= p2 by A2, A9, Th40 ;
thus Hom c,(cod p1) <> {} by A6, CAT_1:19; :: according to CAT_1:def 17 :: thesis: ex b₁ being Morphism of c, cod p1 st b₁ is invertible
take p ; :: thesis: p is invertible
take h ; :: according to CAT_1:def 12 :: thesis: ( dom h = cod p & cod h = dom p & p * h = id (cod p) & h * p = id (dom p) )
thus ( dom h = cod p & cod h = dom p ) by A6, A3, CAT_1:18; :: thesis: ( p * h = id (cod p) & h * p = id (dom p) )
thus p * h = id (cod p) by A3, A4; :: thesis: h * p = id (dom p)
then p1 * (h * p) = (id (cod p)) * p by A6, A5, A7, CAT_1:43
.= p by CAT_1:46 ;
hence id (dom p) = h * p by A1, A6, A13, A12, Th63; :: thesis: verum