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