let C be Category; :: thesis: for c being Object of C

for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

let c be Object of C; :: thesis: for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

let p1, p2 be Morphism of C; :: thesis: ( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

set i1 = p1 opp ;

set i2 = p2 opp ;

thus ( c is_a_product_wrt p1,p2 implies c opp is_a_coproduct_wrt p1 opp ,p2 opp ) :: thesis: ( c opp is_a_coproduct_wrt p1 opp ,p2 opp implies c is_a_product_wrt p1,p2 )

A18: ( cod (p1 opp) = c opp & cod (p2 opp) = c opp ) and

A19: for d being Object of (C opp)

for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) ) ; :: according to CAT_3:def 18 :: thesis: c is_a_product_wrt p1,p2

reconsider gg = p1 as Morphism of dom p1, cod p1 by CAT_1:4;

A20: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A21: gg opp = p1 opp by OPPCAT_1:def 6;

A22: dom p1 = c opp by A18, A20, A21, OPPCAT_1:10;

reconsider gg = p2 as Morphism of dom p2, cod p2 by CAT_1:4;

A23: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A24: gg opp = p2 opp by OPPCAT_1:def 6;

A25: dom p2 = c opp by A18, A23, A24, OPPCAT_1:10;

hence ( dom p1 = c & dom p2 = c ) by A22; :: according to CAT_3:def 15 :: thesis: 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 ) ) )

let d be Object of C; :: thesis: 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 ) ) )

let f, g be Morphism of C; :: thesis: ( f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) implies 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 ) ) ) )

assume that

A26: f in Hom (d,(cod p1)) and

A27: g in Hom (d,(cod p2)) ; :: thesis: 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 ) ) )

g opp in Hom (((cod p2) opp),(d opp)) by A27, OPPCAT_1:5;

then A28: g opp in Hom ((dom (p2 opp)),(d opp)) by A23, A24, OPPCAT_1:12;

f opp in Hom (((cod p1) opp),(d opp)) by A26, OPPCAT_1:5;

then f opp in Hom ((dom (p1 opp)),(d opp)) by A20, A21, OPPCAT_1:12;

then consider h being Morphism of (C opp) such that

A29: h in Hom ((c opp),(d opp)) and

A30: for k being Morphism of (C opp) st k in Hom ((c opp),(d opp)) holds

( ( k (*) (p1 opp) = f opp & k (*) (p2 opp) = g opp ) iff h = k ) by A19, A28;

take opp h ; :: thesis: ( opp 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 opp h = k ) ) )

thus opp h in Hom (d,c) by A29, OPPCAT_1:5; :: thesis: for k being Morphism of C st k in Hom (d,c) holds

( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k )

let k be Morphism of C; :: thesis: ( k in Hom (d,c) implies ( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k ) )

assume A31: k in Hom (d,c) ; :: thesis: ( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k )

then k opp in Hom ((c opp),(d opp)) by OPPCAT_1:5;

then A32: ( ( (k opp) (*) (p1 opp) = f opp & (k opp) (*) (p2 opp) = g opp ) iff h = k opp ) by A30;

A33: cod k = c by A31, CAT_1:1;

reconsider ff = p1 as Morphism of dom p1, cod p1 by CAT_1:4;

reconsider gg = k as Morphism of dom k, dom p1 by A33, A22, CAT_1:4;

A34: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom p1),(cod p1)) <> {} ) by CAT_1:2;

then A35: ff opp = p1 opp by OPPCAT_1:def 6;

A36: gg opp = k opp by A34, A33, A22, OPPCAT_1:def 6;

A37: (p1 (*) k) opp = (k opp) (*) (p1 opp) by A22, A34, A33, A35, A36, OPPCAT_1:16;

reconsider ff = p2 as Morphism of dom p2, cod p2 by CAT_1:4;

reconsider gg = k as Morphism of dom k, dom p2 by A33, A25, CAT_1:4;

A38: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom p2),(cod p2)) <> {} ) by CAT_1:2;

then A39: ff opp = p2 opp by OPPCAT_1:def 6;

A40: gg opp = k opp by A38, A33, A25, OPPCAT_1:def 6;

(p2 (*) k) opp = (k opp) (*) (p2 opp) by A38, A33, A39, A40, A25, OPPCAT_1:16;

hence ( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k ) by A37, A32; :: thesis: verum

for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

let c be Object of C; :: thesis: for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

let p1, p2 be Morphism of C; :: thesis: ( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

set i1 = p1 opp ;

set i2 = p2 opp ;

thus ( c is_a_product_wrt p1,p2 implies c opp is_a_coproduct_wrt p1 opp ,p2 opp ) :: thesis: ( c opp is_a_coproduct_wrt p1 opp ,p2 opp implies c is_a_product_wrt p1,p2 )

proof

assume that
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 ) ) ) ; :: according to CAT_3:def 15 :: thesis: c opp is_a_coproduct_wrt p1 opp ,p2 opp

reconsider gg = p1 as Morphism of dom p1, cod p1 by CAT_1:4;

A3: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A4: gg opp = p1 opp by OPPCAT_1:def 6;

thus A5: cod (p1 opp) = c opp by A1, A3, A4, OPPCAT_1:10; :: according to CAT_3:def 18 :: thesis: ( cod (p2 opp) = c opp & ( for d being Object of (C opp)

for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) ) ) )

reconsider gg = p2 as Morphism of dom p2, cod p2 by CAT_1:4;

A6: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A7: gg opp = p2 opp by OPPCAT_1:def 6;

thus A8: cod (p2 opp) = c opp by A1, A6, A7, OPPCAT_1:10; :: thesis: for d being Object of (C opp)

for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) )

let d be Object of (C opp); :: thesis: for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) )

let f, g be Morphism of (C opp); :: thesis: ( f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) implies ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) ) )

assume that

A9: f in Hom ((dom (p1 opp)),d) and

A10: g in Hom ((dom (p2 opp)),d) ; :: thesis: ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) )

reconsider gg = p2 opp as Morphism of dom (p2 opp), cod (p2 opp) by CAT_1:4;

A11: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

opp g in Hom ((opp d),(opp (dom (p2 opp)))) by A10, OPPCAT_1:6;

then A12: opp g in Hom ((opp d),(cod (opp (p2 opp)))) by A11, OPPCAT_1:13;

reconsider gg = p1 opp as Morphism of dom (p1 opp), cod (p1 opp) by CAT_1:4;

A13: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

opp f in Hom ((opp d),(opp (dom (p1 opp)))) by A9, OPPCAT_1:6;

then opp f in Hom ((opp d),(cod (opp (p1 opp)))) by A13, OPPCAT_1:13;

then consider h being Morphism of C such that

A14: h in Hom ((opp d),c) and

A15: for k being Morphism of C st k in Hom ((opp d),c) holds

( ( p1 (*) k = opp f & p2 (*) k = opp g ) iff h = k ) by A2, A12;

take h opp ; :: thesis: ( h opp in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k ) ) )

h opp in Hom ((c opp),((opp d) opp)) by A14, OPPCAT_1:5;

hence h opp in Hom ((c opp),d) ; :: thesis: for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k )

let k be Morphism of (C opp); :: thesis: ( k in Hom ((c opp),d) implies ( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k ) )

assume A16: k in Hom ((c opp),d) ; :: thesis: ( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k )

then opp k in Hom ((opp d),(opp (c opp))) by OPPCAT_1:6;

then A17: ( ( (opp (p1 opp)) (*) (opp k) = f & (opp (p2 opp)) (*) (opp k) = g ) iff h opp = k ) by A15;

dom k = c opp by A16, CAT_1:1;

then ( ( opp (k (*) (p1 opp)) = f & opp (k (*) (p2 opp)) = g ) iff h opp = k ) by A8, A5, A17, OPPCAT_1:18;

hence ( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k ) ; :: thesis: verum

end;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 ) ) ) ; :: according to CAT_3:def 15 :: thesis: c opp is_a_coproduct_wrt p1 opp ,p2 opp

reconsider gg = p1 as Morphism of dom p1, cod p1 by CAT_1:4;

A3: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A4: gg opp = p1 opp by OPPCAT_1:def 6;

thus A5: cod (p1 opp) = c opp by A1, A3, A4, OPPCAT_1:10; :: according to CAT_3:def 18 :: thesis: ( cod (p2 opp) = c opp & ( for d being Object of (C opp)

for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) ) ) )

reconsider gg = p2 as Morphism of dom p2, cod p2 by CAT_1:4;

A6: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A7: gg opp = p2 opp by OPPCAT_1:def 6;

thus A8: cod (p2 opp) = c opp by A1, A6, A7, OPPCAT_1:10; :: thesis: for d being Object of (C opp)

for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) )

let d be Object of (C opp); :: thesis: for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) )

let f, g be Morphism of (C opp); :: thesis: ( f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) implies ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) ) )

assume that

A9: f in Hom ((dom (p1 opp)),d) and

A10: g in Hom ((dom (p2 opp)),d) ; :: thesis: ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) )

reconsider gg = p2 opp as Morphism of dom (p2 opp), cod (p2 opp) by CAT_1:4;

A11: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

opp g in Hom ((opp d),(opp (dom (p2 opp)))) by A10, OPPCAT_1:6;

then A12: opp g in Hom ((opp d),(cod (opp (p2 opp)))) by A11, OPPCAT_1:13;

reconsider gg = p1 opp as Morphism of dom (p1 opp), cod (p1 opp) by CAT_1:4;

A13: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

opp f in Hom ((opp d),(opp (dom (p1 opp)))) by A9, OPPCAT_1:6;

then opp f in Hom ((opp d),(cod (opp (p1 opp)))) by A13, OPPCAT_1:13;

then consider h being Morphism of C such that

A14: h in Hom ((opp d),c) and

A15: for k being Morphism of C st k in Hom ((opp d),c) holds

( ( p1 (*) k = opp f & p2 (*) k = opp g ) iff h = k ) by A2, A12;

take h opp ; :: thesis: ( h opp in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k ) ) )

h opp in Hom ((c opp),((opp d) opp)) by A14, OPPCAT_1:5;

hence h opp in Hom ((c opp),d) ; :: thesis: for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k )

let k be Morphism of (C opp); :: thesis: ( k in Hom ((c opp),d) implies ( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k ) )

assume A16: k in Hom ((c opp),d) ; :: thesis: ( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k )

then opp k in Hom ((opp d),(opp (c opp))) by OPPCAT_1:6;

then A17: ( ( (opp (p1 opp)) (*) (opp k) = f & (opp (p2 opp)) (*) (opp k) = g ) iff h opp = k ) by A15;

dom k = c opp by A16, CAT_1:1;

then ( ( opp (k (*) (p1 opp)) = f & opp (k (*) (p2 opp)) = g ) iff h opp = k ) by A8, A5, A17, OPPCAT_1:18;

hence ( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h opp = k ) ; :: thesis: verum

A18: ( cod (p1 opp) = c opp & cod (p2 opp) = c opp ) and

A19: for d being Object of (C opp)

for f, g being Morphism of (C opp) st f in Hom ((dom (p1 opp)),d) & g in Hom ((dom (p2 opp)),d) holds

ex h being Morphism of (C opp) st

( h in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds

( ( k (*) (p1 opp) = f & k (*) (p2 opp) = g ) iff h = k ) ) ) ; :: according to CAT_3:def 18 :: thesis: c is_a_product_wrt p1,p2

reconsider gg = p1 as Morphism of dom p1, cod p1 by CAT_1:4;

A20: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A21: gg opp = p1 opp by OPPCAT_1:def 6;

A22: dom p1 = c opp by A18, A20, A21, OPPCAT_1:10;

reconsider gg = p2 as Morphism of dom p2, cod p2 by CAT_1:4;

A23: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;

then A24: gg opp = p2 opp by OPPCAT_1:def 6;

A25: dom p2 = c opp by A18, A23, A24, OPPCAT_1:10;

hence ( dom p1 = c & dom p2 = c ) by A22; :: according to CAT_3:def 15 :: thesis: 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 ) ) )

let d be Object of C; :: thesis: 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 ) ) )

let f, g be Morphism of C; :: thesis: ( f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) implies 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 ) ) ) )

assume that

A26: f in Hom (d,(cod p1)) and

A27: g in Hom (d,(cod p2)) ; :: thesis: 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 ) ) )

g opp in Hom (((cod p2) opp),(d opp)) by A27, OPPCAT_1:5;

then A28: g opp in Hom ((dom (p2 opp)),(d opp)) by A23, A24, OPPCAT_1:12;

f opp in Hom (((cod p1) opp),(d opp)) by A26, OPPCAT_1:5;

then f opp in Hom ((dom (p1 opp)),(d opp)) by A20, A21, OPPCAT_1:12;

then consider h being Morphism of (C opp) such that

A29: h in Hom ((c opp),(d opp)) and

A30: for k being Morphism of (C opp) st k in Hom ((c opp),(d opp)) holds

( ( k (*) (p1 opp) = f opp & k (*) (p2 opp) = g opp ) iff h = k ) by A19, A28;

take opp h ; :: thesis: ( opp 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 opp h = k ) ) )

thus opp h in Hom (d,c) by A29, OPPCAT_1:5; :: thesis: for k being Morphism of C st k in Hom (d,c) holds

( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k )

let k be Morphism of C; :: thesis: ( k in Hom (d,c) implies ( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k ) )

assume A31: k in Hom (d,c) ; :: thesis: ( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k )

then k opp in Hom ((c opp),(d opp)) by OPPCAT_1:5;

then A32: ( ( (k opp) (*) (p1 opp) = f opp & (k opp) (*) (p2 opp) = g opp ) iff h = k opp ) by A30;

A33: cod k = c by A31, CAT_1:1;

reconsider ff = p1 as Morphism of dom p1, cod p1 by CAT_1:4;

reconsider gg = k as Morphism of dom k, dom p1 by A33, A22, CAT_1:4;

A34: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom p1),(cod p1)) <> {} ) by CAT_1:2;

then A35: ff opp = p1 opp by OPPCAT_1:def 6;

A36: gg opp = k opp by A34, A33, A22, OPPCAT_1:def 6;

A37: (p1 (*) k) opp = (k opp) (*) (p1 opp) by A22, A34, A33, A35, A36, OPPCAT_1:16;

reconsider ff = p2 as Morphism of dom p2, cod p2 by CAT_1:4;

reconsider gg = k as Morphism of dom k, dom p2 by A33, A25, CAT_1:4;

A38: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom p2),(cod p2)) <> {} ) by CAT_1:2;

then A39: ff opp = p2 opp by OPPCAT_1:def 6;

A40: gg opp = k opp by A38, A33, A25, OPPCAT_1:def 6;

(p2 (*) k) opp = (k opp) (*) (p2 opp) by A38, A33, A39, A40, A25, OPPCAT_1:16;

hence ( ( p1 (*) k = f & p2 (*) k = g ) iff opp h = k ) by A37, A32; :: thesis: verum