let I be set ; :: thesis: for C being Category
for c being Object of
for F being Function of I,the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
let C be Category; :: thesis: for c being Object of
for F being Function of I,the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
let c be Object of ; :: thesis: for F being Function of I,the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
let F be Function of I,the carrier' of C; :: thesis: ( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
thus ( c is_a_product_wrt F implies c opp is_a_coproduct_wrt F opp ) :: thesis: ( c opp is_a_coproduct_wrt F opp implies c is_a_product_wrt F )

proof

assume A1: c is_a_product_wrt F ; :: thesis: c opp is_a_coproduct_wrt F opp
then F is Projections_family of c,I by Def15;
hence F opp is Injections_family of c opp ,I by Th74; :: according to CAT_3:def 18 :: thesis: for d being Object of
for F' being Injections_family of d,I st doms (F opp ) = doms F' holds
ex h being Morphism of st
( h in Hom (c opp ),d & ( for k being Morphism of st k in Hom (c opp ),d holds
( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) iff h = k ) ) )
let d be Object of ; :: thesis: for F' being Injections_family of d,I st doms (F opp ) = doms F' holds
ex h being Morphism of st
( h in Hom (c opp ),d & ( for k being Morphism of st k in Hom (c opp ),d holds
( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) iff h = k ) ) )
let F' be Injections_family of d,I; :: thesis: ( doms (F opp ) = doms F' implies ex h being Morphism of st
( h in Hom (c opp ),d & ( for k being Morphism of st k in Hom (c opp ),d holds
( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) iff h = k ) ) ) )
assume A2: doms (F opp ) = doms F' ; :: thesis: ex h being Morphism of st
( h in Hom (c opp ),d & ( for k being Morphism of st k in Hom (c opp ),d holds
( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) iff h = k ) ) )
reconsider oppF' = opp F' as Projections_family of opp d,I by Th75;

now

let x be set ; :: thesis: ( x in I implies (cods F) /. x = (cods oppF') /. x )
assume A3: x in I ; :: thesis: (cods F) /. x = (cods oppF') /. x
hence (cods F) /. x = cod (F /. x) by Def4
.= dom ((F /. x) opp ) by OPPCAT_1:9
.= dom ((F opp ) /. x) by A3, Def5
.= (doms F') /. x by A2, A3, Def3
.= dom (F' /. x) by A3, Def3
.= cod (opp (F' /. x)) by OPPCAT_1:10
.= cod (oppF' /. x) by A3, Def6
.= (cods oppF') /. x by A3, Def4 ;
:: thesis: verum

end;

then cods F = cods oppF' by Th1;
then consider h being Morphism of such that
A4: h in Hom (opp d),c and
A5: for k being Morphism of st k in Hom (opp d),c holds
( ( for x being set st x in I holds
(F /. x) * k = oppF' /. x ) iff h = k ) by A1, Def15;
take h opp ; :: thesis: ( h opp in Hom (c opp ),d & ( for k being Morphism of st k in Hom (c opp ),d holds
( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) 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 st k in Hom (c opp ),d holds
( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) iff h opp = k )
let k be Morphism of ; :: thesis: ( k in Hom (c opp ),d implies ( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) iff h opp = k ) )
assume A6: k in Hom (c opp ),d ; :: thesis: ( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) iff h opp = k )
then opp k in Hom (opp d),(opp (c opp )) by OPPCAT_1:14;
then A7: opp k in Hom (opp d),c by OPPCAT_1:4;
thus ( ( for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ) implies h opp = k ) :: thesis: ( h opp = k implies for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x )

proof

assume A8: for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x ; :: thesis: h opp = k

now

let x be set ; :: thesis: ( x in I implies oppF' /. x = (F /. x) * (opp k) )
assume A9: x in I ; :: thesis: oppF' /. x = (F /. x) * (opp k)
F is Projections_family of c,I by A1, Def15;
then dom (F /. x) = c by A9, Th45;
then cod ((F /. x) opp ) = c opp by OPPCAT_1:11;
then cod ((F opp ) /. x) = c opp by A9, Def5;
then A10: dom k = cod ((F opp ) /. x) by A6, CAT_1:18;
opp (k * ((F opp ) /. x)) = opp (F' /. x) by A8, A9;
hence oppF' /. x = opp (k * ((F opp ) /. x)) by A9, Def6
.= (opp ((F opp ) /. x)) * (opp k) by A10, OPPCAT_1:19
.= (opp ((F /. x) opp )) * (opp k) by A9, Def5
.= (F /. x) * (opp k) by OPPCAT_1:7 ;
:: thesis: verum

end;

then h = opp k by A5, A7;
hence h opp = k by OPPCAT_1:8; :: thesis: verum

end;

assume h opp = k ; :: thesis: for x being set st x in I holds
k * ((F opp ) /. x) = F' /. x
then A11: h = opp k by OPPCAT_1:7;
let x be set ; :: thesis: ( x in I implies k * ((F opp ) /. x) = F' /. x )
assume A12: x in I ; :: thesis: k * ((F opp ) /. x) = F' /. x
F is Projections_family of c,I by A1, Def15;
then dom (F /. x) = c by A12, Th45;
then A13: cod (opp k) = dom (F /. x) by A7, CAT_1:18;
(F /. x) * (opp k) = oppF' /. x by A5, A7, A12, A11;
then ((opp k) opp ) * ((F /. x) opp ) = (oppF' /. x) opp by A13, OPPCAT_1:17;
then k * ((F /. x) opp ) = (oppF' /. x) opp by OPPCAT_1:8;
hence k * ((F opp ) /. x) = (oppF' /. x) opp by A12, Def5
.= (opp (F' /. x)) opp by A12, Def6
.= F' /. x by OPPCAT_1:8 ;
:: thesis: verum

end;

assume A14: c opp is_a_coproduct_wrt F opp ; :: thesis: c is_a_product_wrt F
then F opp is Injections_family of c opp ,I by Def18;
hence F is Projections_family of c,I by Th74; :: according to CAT_3:def 15 :: thesis: for b being Object of
for F' being Projections_family of b,I st cods F = cods F' holds
ex h being Morphism of st
( h in Hom b,c & ( for k being Morphism of st k in Hom b,c holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff h = k ) ) )
let d be Object of ; :: thesis: for F' being Projections_family of d,I st cods F = cods F' holds
ex h being Morphism of st
( h in Hom d,c & ( for k being Morphism of st k in Hom d,c holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff h = k ) ) )
let F' be Projections_family of d,I; :: thesis: ( cods F = cods F' implies ex h being Morphism of st
( h in Hom d,c & ( for k being Morphism of st k in Hom d,c holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff h = k ) ) ) )
assume A15: cods F = cods F' ; :: thesis: ex h being Morphism of st
( h in Hom d,c & ( for k being Morphism of st k in Hom d,c holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff h = k ) ) )

A16: now

let x be set ; :: thesis: ( x in I implies (doms (F opp )) /. x = (doms (F' opp )) /. x )
assume A17: x in I ; :: thesis: (doms (F opp )) /. x = (doms (F' opp )) /. x
hence (doms (F opp )) /. x = dom ((F opp ) /. x) by Def3
.= dom ((F /. x) opp ) by A17, Def5
.= cod (F /. x) by OPPCAT_1:9
.= (cods F') /. x by A15, A17, Def4
.= cod (F' /. x) by A17, Def4
.= dom ((F' /. x) opp ) by OPPCAT_1:9
.= dom ((F' opp ) /. x) by A17, Def5
.= (doms (F' opp )) /. x by A17, Def3 ;
:: thesis: verum

end;

reconsider F'opp = F' opp as Injections_family of d opp ,I by Th74;
doms (F opp ) = doms F'opp by A16, Th1;
then consider h being Morphism of such that
A18: h in Hom (c opp ),(d opp ) and
A19: for k being Morphism of st k in Hom (c opp ),(d opp ) holds
( ( for x being set st x in I holds
k * ((F opp ) /. x) = F'opp /. x ) iff h = k ) by A14, Def18;
take opp h ; :: thesis: ( opp h in Hom d,c & ( for k being Morphism of st k in Hom d,c holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff opp h = k ) ) )
opp h in Hom (opp (d opp )),(opp (c opp )) by A18, OPPCAT_1:14;
then opp h in Hom d,(opp (c opp )) by OPPCAT_1:4;
hence opp h in Hom d,c by OPPCAT_1:4; :: thesis: for k being Morphism of st k in Hom d,c holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff opp h = k )
let k be Morphism of ; :: thesis: ( k in Hom d,c implies ( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff opp h = k ) )
assume A20: k in Hom d,c ; :: thesis: ( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff opp h = k )
then A21: k opp in Hom (c opp ),(d opp ) by OPPCAT_1:13;
thus ( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) implies opp h = k ) :: thesis: ( opp h = k implies for x being set st x in I holds
(F /. x) * k = F' /. x )

proof

assume A22: for x being set st x in I holds
(F /. x) * k = F' /. x ; :: thesis: opp h = k

now

let x be set ; :: thesis: ( x in I implies F'opp /. x = (k opp ) * ((F opp ) /. x) )
assume A23: x in I ; :: thesis: F'opp /. x = (k opp ) * ((F opp ) /. x)
F opp is Injections_family of c opp ,I by A14, Def18;
then cod ((F opp ) /. x) = c opp by A23, Th67;
then cod ((F /. x) opp ) = c opp by A23, Def5;
then dom (F /. x) = c opp by OPPCAT_1:9;
then dom (F /. x) = c by OPPCAT_1:def 2;
then A24: cod k = dom (F /. x) by A20, CAT_1:18;
(F /. x) * k = F' /. x by A22, A23;
then (k opp ) * ((F /. x) opp ) = (F' /. x) opp by A24, OPPCAT_1:17;
hence F'opp /. x = (k opp ) * ((F /. x) opp ) by A23, Def5
.= (k opp ) * ((F opp ) /. x) by A23, Def5 ;
:: thesis: verum

end;

then h = k opp by A19, A21;
hence opp h = k by OPPCAT_1:7; :: thesis: verum

end;

assume opp h = k ; :: thesis: for x being set st x in I holds
(F /. x) * k = F' /. x
then A25: h = k opp by OPPCAT_1:8;
let x be set ; :: thesis: ( x in I implies (F /. x) * k = F' /. x )
assume A26: x in I ; :: thesis: (F /. x) * k = F' /. x
F opp is Injections_family of c opp ,I by A14, Def18;
then cod ((F opp ) /. x) = c opp by A26, Th67;
then cod ((F /. x) opp ) = c opp by A26, Def5;
then dom (F /. x) = c opp by OPPCAT_1:9;
then dom (F /. x) = c by OPPCAT_1:def 2;
then A27: cod k = dom (F /. x) by A20, CAT_1:18;
(k opp ) * ((F opp ) /. x) = F'opp /. x by A19, A21, A26, A25;
then (k opp ) * ((F opp ) /. x) = (F' /. x) opp by A26, Def5;
hence F' /. x = (k opp ) * ((F opp ) /. x) by OPPCAT_1:def 4
.= (k opp ) * ((F /. x) opp ) by A26, Def5
.= ((F /. x) * k) opp by A27, OPPCAT_1:17
.= (F /. x) * k by OPPCAT_1:def 4 ;
:: thesis: verum