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 )

proof

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 14 :: thesis: c opp is_a_coproduct_wrt p1 opp ,p2 opp
( dom p1 = c opp & dom p2 = c opp ) by A1, OPPCAT_1:def 2;
hence A3: ( cod (p1 opp) = c opp & cod (p2 opp) = c opp ) by OPPCAT_1:8; :: according to CAT_3:def 17 :: 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
A4: f in Hom ((dom (p1 opp)),d) and
A5: 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 ) ) )
opp g in Hom ((opp d),(opp (dom (p2 opp)))) by A5, OPPCAT_1:13;
then opp g in Hom ((opp d),(cod (opp (p2 opp)))) by OPPCAT_1:11;
then A6: opp g in Hom ((opp d),(cod p2)) by OPPCAT_1:6;
opp f in Hom ((opp d),(opp (dom (p1 opp)))) by A4, OPPCAT_1:13;
then opp f in Hom ((opp d),(cod (opp (p1 opp)))) by OPPCAT_1:11;
then opp f in Hom ((opp d),(cod p1)) by OPPCAT_1:6;
then consider h being Morphism of C such that
A7: h in Hom ((opp d),c) and
A8: 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, A6;
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 A7, OPPCAT_1:12;
hence h opp in Hom ((c opp),d) by OPPCAT_1:4; :: 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 A9: 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:13;
then opp k in Hom ((opp d),c) by OPPCAT_1:3;
then ( ( p1 * (opp k) = opp f & p2 * (opp k) = opp g ) iff h = opp k ) by A8;
then ( ( p1 * (opp k) = f opp & p2 * (opp k) = g opp ) iff h = k opp ) by OPPCAT_1:def 5;
then ( ( p1 * (opp k) = f & p2 * (opp k) = g ) iff h = k ) by OPPCAT_1:def 4;
then A10: ( ( (opp (p1 opp)) * (opp k) = f & (opp (p2 opp)) * (opp k) = g ) iff h opp = k ) by OPPCAT_1:6, OPPCAT_1:def 4;
dom k = c opp by A9, CAT_1:1;
then ( ( opp (k * (p1 opp)) = f & opp (k * (p2 opp)) = g ) iff h opp = k ) by A3, A10, OPPCAT_1:18;
then ( ( (k * (p1 opp)) opp = f & (k * (p2 opp)) opp = g ) iff h opp = k ) by OPPCAT_1:def 5;
hence ( ( k * (p1 opp) = f & k * (p2 opp) = g ) iff h opp = k ) by OPPCAT_1:def 4; :: thesis: verum

end;

assume that
A11: ( cod (p1 opp) = c opp & cod (p2 opp) = c opp ) and
A12: 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 17 :: thesis: c is_a_product_wrt p1,p2
A13: ( dom p1 = c opp & dom p2 = c opp ) by A11, OPPCAT_1:8;
hence ( dom p1 = c & dom p2 = c ) by OPPCAT_1:def 2; :: according to CAT_3:def 14 :: 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
A14: f in Hom (d,(cod p1)) and
A15: 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 A15, OPPCAT_1:12;
then A16: g opp in Hom ((dom (p2 opp)),(d opp)) by OPPCAT_1:10;
f opp in Hom (((cod p1) opp),(d opp)) by A14, OPPCAT_1:12;
then f opp in Hom ((dom (p1 opp)),(d opp)) by OPPCAT_1:10;
then consider h being Morphism of (C opp) such that
A17: h in Hom ((c opp),(d opp)) and
A18: 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 A12, A16;
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 ) ) )
h = (opp h) opp by OPPCAT_1:7;
hence opp h in Hom (d,c) by A17, OPPCAT_1:12; :: 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 A19: 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:12;
then ( ( (k opp) * (p1 opp) = f opp & (k opp) * (p2 opp) = g opp ) iff h = k opp ) by A18;
then A20: ( ( (k opp) * (p1 opp) = f & (k opp) * (p2 opp) = g ) iff h opp = k opp ) by OPPCAT_1:def 4;
cod k = c by A19, CAT_1:1;
then ( ( (p1 * k) opp = f & (p2 * k) opp = g ) iff h opp = k ) by A13, A20, OPPCAT_1:16, OPPCAT_1:def 2, OPPCAT_1:def 4;
hence ( ( p1 * k = f & p2 * k = g ) iff opp h = k ) by OPPCAT_1:def 4, OPPCAT_1:def 5; :: thesis: verum