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 p1 is terminal holds

c, cod p2 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 p1 is terminal holds

c, cod p2 are_isomorphic

let p1, p2 be Morphism of C; :: thesis: ( 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 ; :: thesis: 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 ; :: according to CAT_1:def 20 :: thesis: p is invertible

thus ( Hom (c,(cod p2)) <> {} & Hom ((cod p2),c) <> {} ) by A6, A3, CAT_1:2; :: according to CAT_1:def 16 :: thesis: ex b_{1} being Morphism of cod p2,c st

( p * b_{1} = id (cod p2) & b_{1} * p = id c )

reconsider h = h as Morphism of cod p2,c by A3, CAT_1:def 5;

take h ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: according to CAT_1:def 20 :: thesis: p is invertible

thus ( Hom (c,(cod p2)) <> {} & Hom ((cod p2),c) <> {} ) by A6, A3, CAT_1:2; :: according to CAT_1:def 16 :: thesis: ex b

( p * b

reconsider h = h as Morphism of cod p2,c by A3, CAT_1:def 5;

take h ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum