let C be Category; for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p1 is terminal holds
c, cod p2 are_isomorphic
let c be Object of C; for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p1 is terminal holds
c, cod p2 are_isomorphic
let p1, p2 be Morphism of C; ( c is_a_product_wrt p1,p2 & cod p1 is terminal implies c, cod p2 are_isomorphic )
set a = cod p1;
set b = cod p2;
assume that
A1:
c is_a_product_wrt p1,p2
and
A2:
cod p1 is terminal
; c, cod p2 are_isomorphic
set f = id (cod p2);
set g = term ((cod p2),(cod p1));
( dom (term ((cod p2),(cod p1))) = cod p2 & cod (term ((cod p2),(cod p1))) = cod p1 )
by A2, Th35;
then
( id (cod p2) in Hom ((cod p2),(cod p2)) & term ((cod p2),(cod p1)) in Hom ((cod p2),(cod p1)) )
by CAT_1:27;
then consider h being Morphism of C such that
A3:
h in Hom ((cod p2),c)
and
A4:
for k being Morphism of C st k in Hom ((cod p2),c) holds
( ( p1 (*) k = term ((cod p2),(cod p1)) & p2 (*) k = id (cod p2) ) iff h = k )
by A1;
A5:
dom h = cod p2
by A3, CAT_1:1;
A6:
dom p2 = c
by A1;
then reconsider p = p2 as Morphism of c, cod p2 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 p1 = c
by A1;
then A10:
cod (p1 (*) (h (*) p)) = cod p1
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 (p1 (*) (h (*) p)) = c
by A9, A11, A8, CAT_1:17;
then A13: p1 (*) (h (*) p) =
term (c,(cod p1))
by A2, A10, Th36
.=
p1
by A2, A9, Th36
;
A14:
Hom (c,(cod p2)) <> {}
by A6, CAT_1:2;
take
p
; CAT_1:def 20 p is invertible
thus
( Hom (c,(cod p2)) <> {} & Hom ((cod p2),c) <> {} )
by A6, A3, CAT_1:2; CAT_1:def 16 ex b1 being Morphism of cod p2,c st
( p * b1 = id (cod p2) & b1 * p = id c )
reconsider h = h as Morphism of cod p2,c by A3, CAT_1:def 5;
take
h
; ( p * h = id (cod p2) & h * p = id c )
thus p * h =
p (*) h
by A14, A3, CAT_1:def 13
.=
id (cod p2)
by A3, A4
; h * p = id c
p (*) h = id (cod p)
by A3, A4;
then A15: p2 (*) (h (*) p) =
(id (cod p)) (*) p
by A6, A5, A7, CAT_1:18
.=
p
by CAT_1:21
;
thus id c =
h (*) p
by A1, A13, A12, Th58, A15
.=
h * p
by A14, A3, CAT_1:def 13
; verum