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, Th35;
then ( id (cod p1) in Hom ((cod p1),(cod p1)) & term ((cod p1),(cod p2)) in Hom ((cod p1),(cod p2)) ) by CAT_1:27;
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;
A5: dom h = cod p1 by A3, CAT_1:1;
reconsider h = h as Morphism of cod p1,c by A3, CAT_1:def 5;
A6: dom p1 = c by A1;
then reconsider p = p1 as Morphism of c, cod p1 by CAT_1:4;
A7: cod h = c by A3, CAT_1:1;
then A8: cod (h (*) p) = c by A5, CAT_1:17;
A9: dom p2 = c by A1;
then A10: cod (p2 (*) (h (*) p)) = cod p2 by A8, CAT_1:17;
A11: dom (h (*) p) = c by A6, A5, CAT_1:17;
then A12: h (*) p in Hom (c,c) by A8;
dom (p2 (*) (h (*) p)) = c by A9, A11, A8, CAT_1:17;
then A13: p2 (*) (h (*) p) = term (c,(cod p2)) by A2, A10, Th36
.= p2 by A2, A9, Th36 ;
A14: Hom (c,(cod p1)) <> {} by A6, CAT_1:2;
take p ; :: according to CAT_1:def 20 :: thesis: p is invertible
thus ( Hom (c,(cod p1)) <> {} & Hom ((cod p1),c) <> {} ) by A3, A6, CAT_1:2; :: according to CAT_1:def 16 :: thesis: ex b₁ being Morphism of cod p1,c st
( p * b₁ = id (cod p1) & b₁ * p = id c )
take h ; :: thesis: ( p * h = id (cod p1) & h * p = id c )
thus p * h = p (*) h by A3, A14, CAT_1:def 13
.= id (cod p1) by A3, A4 ; :: thesis: h * p = id c
p1 (*) (h (*) p) = (p1 (*) h) (*) p by A6, A5, A7, CAT_1:18
.= (id (cod p)) (*) p by A3, A4
.= p by CAT_1:21 ;
hence id c = h (*) p by A1, A13, A12, Th58
.= h * p by A3, A14, CAT_1:def 13 ;
:: thesis: verum