let I be set ; :: thesis: for C being Category

for c being Object of C

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 C

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 C; :: 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 )

then F opp is Injections_family of c opp ,I ;

hence F is Projections_family of c,I by Th68; :: according to CAT_3:def 14 :: thesis: for b being Object of C

for F9 being Projections_family of b,I st cods F = cods F9 holds

ex h being Morphism of C st

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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) )

let d be Object of C; :: thesis: for F9 being Projections_family of d,I st cods F = cods F9 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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) )

let F9 be Projections_family of d,I; :: thesis: ( cods F = cods F9 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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) )

assume A23: cods F = cods F9 ; :: 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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) )

consider h being Morphism of (C opp) such that

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

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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9opp /. x ) iff h = k ) by A22, A24, Th1;

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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k ) ) )

opp h in Hom ((opp (d opp)),(opp (c opp))) by A30, OPPCAT_1:6;

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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k )

let k be Morphism of C; :: thesis: ( k in Hom (d,c) implies ( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k ) )

assume A32: k in Hom (d,c) ; :: thesis: ( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k )

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

thus ( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) implies opp h = k ) :: thesis: ( opp h = k implies for x being set st x in I holds

(F /. x) (*) k = F9 /. x )

(F /. x) (*) k = F9 /. x

let x be set ; :: thesis: ( x in I implies (F /. x) (*) k = F9 /. x )

assume A43: x in I ; :: thesis: (F /. x) (*) k = F9 /. x

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A45: gg opp = (F /. x) opp by OPPCAT_1:def 6;

F opp is Injections_family of c opp ,I by A22;

then cod ((F opp) /. x) = c opp by A43, Th62;

then cod (gg opp) = c opp by A43, Def3, A45;

then dom (F /. x) = c by A44, OPPCAT_1:10;

then A46: cod k = dom (F /. x) by A32, CAT_1:1;

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

reconsider gg = F /. x as Morphism of cod k, cod (F /. x) by A46, CAT_1:4;

A47: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A48: ff opp = k opp by OPPCAT_1:def 6;

A49: gg opp = (F /. x) opp by A47, A46, OPPCAT_1:def 6;

(k opp) (*) ((F opp) /. x) = F9opp /. x by A31, A33, A43, A42;

then (k opp) (*) ((F opp) /. x) = (F9 /. x) opp by A43, Def3;

hence F9 /. x = (k opp) (*) ((F /. x) opp) by A43, Def3

.= ((F /. x) (*) k) opp by A46, A48, A49, A47, OPPCAT_1:16

.= (F /. x) (*) k ;

:: thesis: verum

for c being Object of C

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 C

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 C; :: 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 A22:
c opp is_a_coproduct_wrt F opp
; :: thesis: c is_a_product_wrt F
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 ;

hence F opp is Injections_family of c opp ,I by Th68; :: according to CAT_3:def 17 :: thesis: for d being Object of (C opp)

for F9 being Injections_family of d,I st doms (F opp) = doms F9 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )

let d be Object of (C opp); :: thesis: for F9 being Injections_family of d,I st doms (F opp) = doms F9 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )

let F9 be Injections_family of d,I; :: thesis: ( doms (F opp) = doms F9 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) ) )

assume A2: doms (F opp) = doms F9 ; :: 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )

reconsider oppF9 = opp F9 as Projections_family of opp d,I by Th69;

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

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

( ( for x being set st x in I holds

(F /. x) (*) k = oppF9 /. x ) iff h = k ) by A1, Th1;

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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k ) ) )

h in Hom ((c opp),((opp d) opp)) by A7, 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k )

let k be Morphism of (C opp); :: thesis: ( k in Hom ((c opp),d) implies ( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k ) )

assume A9: k in Hom ((c opp),d) ; :: thesis: ( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k )

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

thus ( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) implies h opp = k ) :: thesis: ( h opp = k implies for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x )

k (*) ((F opp) /. x) = F9 /. x

let x be set ; :: thesis: ( x in I implies k (*) ((F opp) /. x) = F9 /. x )

assume A17: x in I ; :: thesis: k (*) ((F opp) /. x) = F9 /. x

F is Projections_family of c,I by A1;

then dom (F /. x) = c by A17, Th41;

then A18: cod (opp k) = dom (F /. x) by A10, CAT_1:1;

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

reconsider gg = F /. x as Morphism of cod (opp k), cod (F /. x) by A18, CAT_1:4;

A19: ( Hom ((dom (opp k)),(cod (opp k))) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A20: ff opp = (opp k) opp by OPPCAT_1:def 6;

A21: gg opp = (F /. x) opp by A19, A18, OPPCAT_1:def 6;

(F /. x) (*) (opp k) = oppF9 /. x by A8, A10, A17, A16;

then ((opp k) opp) (*) ((F /. x) opp) = (oppF9 /. x) opp by A18, A20, A21, A19, OPPCAT_1:16;

hence k (*) ((F opp) /. x) = (oppF9 /. x) opp by A17, Def3

.= (opp (F9 /. x)) opp by A17, Def4

.= F9 /. x ;

:: thesis: verum

end;then F is Projections_family of c,I ;

hence F opp is Injections_family of c opp ,I by Th68; :: according to CAT_3:def 17 :: thesis: for d being Object of (C opp)

for F9 being Injections_family of d,I st doms (F opp) = doms F9 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )

let d be Object of (C opp); :: thesis: for F9 being Injections_family of d,I st doms (F opp) = doms F9 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )

let F9 be Injections_family of d,I; :: thesis: ( doms (F opp) = doms F9 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) ) )

assume A2: doms (F opp) = doms F9 ; :: 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )

reconsider oppF9 = opp F9 as Projections_family of opp d,I by Th69;

now :: thesis: for x being set st x in I holds

(cods F) /. x = (cods oppF9) /. x

then consider h being Morphism of C such that (cods F) /. x = (cods oppF9) /. x

let x be set ; :: thesis: ( x in I implies (cods F) /. x = (cods oppF9) /. x )

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A4: gg opp = (F /. x) opp by OPPCAT_1:def 6;

reconsider g9 = F9 /. x as Morphism of dom (F9 /. x), cod (F9 /. x) by CAT_1:4;

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

then A5: g9 opp = (F9 /. x) opp by OPPCAT_1:def 6;

assume A6: x in I ; :: thesis: (cods F) /. x = (cods oppF9) /. x

hence (cods F) /. x = cod (F /. x) by Def2

.= dom (gg opp) by A3, OPPCAT_1:10

.= dom ((F opp) /. x) by A6, Def3, A4

.= (doms F9) /. x by A2, A6, Def1

.= dom (F9 /. x) by A6, Def1

.= cod (opp (F9 /. x)) by A5, OPPCAT_1:11

.= cod (oppF9 /. x) by A6, Def4

.= (cods oppF9) /. x by A6, Def2 ;

:: thesis: verum

end;reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A4: gg opp = (F /. x) opp by OPPCAT_1:def 6;

reconsider g9 = F9 /. x as Morphism of dom (F9 /. x), cod (F9 /. x) by CAT_1:4;

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

then A5: g9 opp = (F9 /. x) opp by OPPCAT_1:def 6;

assume A6: x in I ; :: thesis: (cods F) /. x = (cods oppF9) /. x

hence (cods F) /. x = cod (F /. x) by Def2

.= dom (gg opp) by A3, OPPCAT_1:10

.= dom ((F opp) /. x) by A6, Def3, A4

.= (doms F9) /. x by A2, A6, Def1

.= dom (F9 /. x) by A6, Def1

.= cod (opp (F9 /. x)) by A5, OPPCAT_1:11

.= cod (oppF9 /. x) by A6, Def4

.= (cods oppF9) /. x by A6, Def2 ;

:: thesis: verum

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

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

( ( for x being set st x in I holds

(F /. x) (*) k = oppF9 /. x ) iff h = k ) by A1, Th1;

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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k ) ) )

h in Hom ((c opp),((opp d) opp)) by A7, 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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k )

let k be Morphism of (C opp); :: thesis: ( k in Hom ((c opp),d) implies ( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k ) )

assume A9: k in Hom ((c opp),d) ; :: thesis: ( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k )

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

thus ( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ) implies h opp = k ) :: thesis: ( h opp = k implies for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x )

proof

assume A16:
h opp = k
; :: thesis: for x being set st x in I holds
assume A11:
for x being set st x in I holds

k (*) ((F opp) /. x) = F9 /. x ; :: thesis: h opp = k

end;k (*) ((F opp) /. x) = F9 /. x ; :: thesis: h opp = k

now :: thesis: for x being set st x in I holds

oppF9 /. x = (F /. x) (*) (opp k)

hence
h opp = k
by A8, A10; :: thesis: verumoppF9 /. x = (F /. x) (*) (opp k)

let x be set ; :: thesis: ( x in I implies oppF9 /. x = (F /. x) (*) (opp k) )

assume A12: x in I ; :: thesis: oppF9 /. x = (F /. x) (*) (opp k)

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A14: gg opp = (F /. x) opp by OPPCAT_1:def 6;

F is Projections_family of c,I by A1;

then dom (F /. x) = c by A12, Th41;

then cod ((F /. x) opp) = c opp by A13, A14, OPPCAT_1:12;

then cod ((F opp) /. x) = c opp by A12, Def3;

then A15: dom k = cod ((F opp) /. x) by A9, CAT_1:1;

opp (k (*) ((F opp) /. x)) = opp (F9 /. x) by A11, A12;

hence oppF9 /. x = opp (k (*) ((F opp) /. x)) by A12, Def4

.= (opp ((F opp) /. x)) (*) (opp k) by A15, OPPCAT_1:18

.= (opp ((F /. x) opp)) (*) (opp k) by A12, Def3

.= (F /. x) (*) (opp k) ;

:: thesis: verum

end;assume A12: x in I ; :: thesis: oppF9 /. x = (F /. x) (*) (opp k)

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A14: gg opp = (F /. x) opp by OPPCAT_1:def 6;

F is Projections_family of c,I by A1;

then dom (F /. x) = c by A12, Th41;

then cod ((F /. x) opp) = c opp by A13, A14, OPPCAT_1:12;

then cod ((F opp) /. x) = c opp by A12, Def3;

then A15: dom k = cod ((F opp) /. x) by A9, CAT_1:1;

opp (k (*) ((F opp) /. x)) = opp (F9 /. x) by A11, A12;

hence oppF9 /. x = opp (k (*) ((F opp) /. x)) by A12, Def4

.= (opp ((F opp) /. x)) (*) (opp k) by A15, OPPCAT_1:18

.= (opp ((F /. x) opp)) (*) (opp k) by A12, Def3

.= (F /. x) (*) (opp k) ;

:: thesis: verum

k (*) ((F opp) /. x) = F9 /. x

let x be set ; :: thesis: ( x in I implies k (*) ((F opp) /. x) = F9 /. x )

assume A17: x in I ; :: thesis: k (*) ((F opp) /. x) = F9 /. x

F is Projections_family of c,I by A1;

then dom (F /. x) = c by A17, Th41;

then A18: cod (opp k) = dom (F /. x) by A10, CAT_1:1;

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

reconsider gg = F /. x as Morphism of cod (opp k), cod (F /. x) by A18, CAT_1:4;

A19: ( Hom ((dom (opp k)),(cod (opp k))) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A20: ff opp = (opp k) opp by OPPCAT_1:def 6;

A21: gg opp = (F /. x) opp by A19, A18, OPPCAT_1:def 6;

(F /. x) (*) (opp k) = oppF9 /. x by A8, A10, A17, A16;

then ((opp k) opp) (*) ((F /. x) opp) = (oppF9 /. x) opp by A18, A20, A21, A19, OPPCAT_1:16;

hence k (*) ((F opp) /. x) = (oppF9 /. x) opp by A17, Def3

.= (opp (F9 /. x)) opp by A17, Def4

.= F9 /. x ;

:: thesis: verum

then F opp is Injections_family of c opp ,I ;

hence F is Projections_family of c,I by Th68; :: according to CAT_3:def 14 :: thesis: for b being Object of C

for F9 being Projections_family of b,I st cods F = cods F9 holds

ex h being Morphism of C st

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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) )

let d be Object of C; :: thesis: for F9 being Projections_family of d,I st cods F = cods F9 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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) )

let F9 be Projections_family of d,I; :: thesis: ( cods F = cods F9 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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) )

assume A23: cods F = cods F9 ; :: 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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) )

A24: now :: thesis: for x being set st x in I holds

(doms (F opp)) /. x = (doms (F9 opp)) /. x

reconsider F9opp = F9 opp as Injections_family of d opp ,I by Th68;(doms (F opp)) /. x = (doms (F9 opp)) /. x

let x be set ; :: thesis: ( x in I implies (doms (F opp)) /. x = (doms (F9 opp)) /. x )

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A26: gg opp = (F /. x) opp by OPPCAT_1:def 6;

reconsider g9 = F9 /. x as Morphism of dom (F9 /. x), cod (F9 /. x) by CAT_1:4;

A27: Hom ((dom g9),(cod g9)) <> {} by CAT_1:2;

then A28: g9 opp = (F9 /. x) opp by OPPCAT_1:def 6;

assume A29: x in I ; :: thesis: (doms (F opp)) /. x = (doms (F9 opp)) /. x

hence (doms (F opp)) /. x = dom ((F opp) /. x) by Def1

.= dom (gg opp) by A29, Def3, A26

.= cod (F /. x) by A25, OPPCAT_1:10

.= (cods F9) /. x by A23, A29, Def2

.= cod (F9 /. x) by A29, Def2

.= dom (g9 opp) by A27, OPPCAT_1:10

.= dom ((F9 opp) /. x) by A29, Def3, A28

.= (doms (F9 opp)) /. x by A29, Def1 ;

:: thesis: verum

end;reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A26: gg opp = (F /. x) opp by OPPCAT_1:def 6;

reconsider g9 = F9 /. x as Morphism of dom (F9 /. x), cod (F9 /. x) by CAT_1:4;

A27: Hom ((dom g9),(cod g9)) <> {} by CAT_1:2;

then A28: g9 opp = (F9 /. x) opp by OPPCAT_1:def 6;

assume A29: x in I ; :: thesis: (doms (F opp)) /. x = (doms (F9 opp)) /. x

hence (doms (F opp)) /. x = dom ((F opp) /. x) by Def1

.= dom (gg opp) by A29, Def3, A26

.= cod (F /. x) by A25, OPPCAT_1:10

.= (cods F9) /. x by A23, A29, Def2

.= cod (F9 /. x) by A29, Def2

.= dom (g9 opp) by A27, OPPCAT_1:10

.= dom ((F9 opp) /. x) by A29, Def3, A28

.= (doms (F9 opp)) /. x by A29, Def1 ;

:: thesis: verum

consider h being Morphism of (C opp) such that

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

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

( ( for x being set st x in I holds

k (*) ((F opp) /. x) = F9opp /. x ) iff h = k ) by A22, A24, Th1;

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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k ) ) )

opp h in Hom ((opp (d opp)),(opp (c opp))) by A30, OPPCAT_1:6;

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

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k )

let k be Morphism of C; :: thesis: ( k in Hom (d,c) implies ( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k ) )

assume A32: k in Hom (d,c) ; :: thesis: ( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff opp h = k )

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

thus ( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) implies opp h = k ) :: thesis: ( opp h = k implies for x being set st x in I holds

(F /. x) (*) k = F9 /. x )

proof

assume A42:
opp h = k
; :: thesis: for x being set st x in I holds
assume A34:
for x being set st x in I holds

(F /. x) (*) k = F9 /. x ; :: thesis: opp h = k

end;(F /. x) (*) k = F9 /. x ; :: thesis: opp h = k

now :: thesis: for x being set st x in I holds

F9opp /. x = (k opp) (*) ((F opp) /. x)

hence
opp h = k
by A31, A33; :: thesis: verumF9opp /. x = (k opp) (*) ((F opp) /. x)

let x be set ; :: thesis: ( x in I implies F9opp /. x = (k opp) (*) ((F opp) /. x) )

assume A35: x in I ; :: thesis: F9opp /. x = (k opp) (*) ((F opp) /. x)

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A37: gg opp = (F /. x) opp by OPPCAT_1:def 6;

F opp is Injections_family of c opp ,I by A22;

then cod ((F opp) /. x) = c opp by A35, Th62;

then cod (gg opp) = c opp by A35, Def3, A37;

then dom (F /. x) = c by A36, OPPCAT_1:10;

then A38: cod k = dom (F /. x) by A32, CAT_1:1;

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

reconsider gg = F /. x as Morphism of cod k, cod (F /. x) by A38, CAT_1:4;

A39: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A40: ff opp = k opp by OPPCAT_1:def 6;

A41: gg opp = (F /. x) opp by A39, A38, OPPCAT_1:def 6;

(F /. x) (*) k = F9 /. x by A34, A35;

then (k opp) (*) ((F /. x) opp) = (F9 /. x) opp by A38, A40, A41, A39, OPPCAT_1:16;

hence F9opp /. x = (k opp) (*) ((F /. x) opp) by A35, Def3

.= (k opp) (*) ((F opp) /. x) by A35, Def3 ;

:: thesis: verum

end;assume A35: x in I ; :: thesis: F9opp /. x = (k opp) (*) ((F opp) /. x)

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A37: gg opp = (F /. x) opp by OPPCAT_1:def 6;

F opp is Injections_family of c opp ,I by A22;

then cod ((F opp) /. x) = c opp by A35, Th62;

then cod (gg opp) = c opp by A35, Def3, A37;

then dom (F /. x) = c by A36, OPPCAT_1:10;

then A38: cod k = dom (F /. x) by A32, CAT_1:1;

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

reconsider gg = F /. x as Morphism of cod k, cod (F /. x) by A38, CAT_1:4;

A39: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A40: ff opp = k opp by OPPCAT_1:def 6;

A41: gg opp = (F /. x) opp by A39, A38, OPPCAT_1:def 6;

(F /. x) (*) k = F9 /. x by A34, A35;

then (k opp) (*) ((F /. x) opp) = (F9 /. x) opp by A38, A40, A41, A39, OPPCAT_1:16;

hence F9opp /. x = (k opp) (*) ((F /. x) opp) by A35, Def3

.= (k opp) (*) ((F opp) /. x) by A35, Def3 ;

:: thesis: verum

(F /. x) (*) k = F9 /. x

let x be set ; :: thesis: ( x in I implies (F /. x) (*) k = F9 /. x )

assume A43: x in I ; :: thesis: (F /. x) (*) k = F9 /. x

reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;

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

then A45: gg opp = (F /. x) opp by OPPCAT_1:def 6;

F opp is Injections_family of c opp ,I by A22;

then cod ((F opp) /. x) = c opp by A43, Th62;

then cod (gg opp) = c opp by A43, Def3, A45;

then dom (F /. x) = c by A44, OPPCAT_1:10;

then A46: cod k = dom (F /. x) by A32, CAT_1:1;

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

reconsider gg = F /. x as Morphism of cod k, cod (F /. x) by A46, CAT_1:4;

A47: ( Hom ((dom k),(cod k)) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A48: ff opp = k opp by OPPCAT_1:def 6;

A49: gg opp = (F /. x) opp by A47, A46, OPPCAT_1:def 6;

(k opp) (*) ((F opp) /. x) = F9opp /. x by A31, A33, A43, A42;

then (k opp) (*) ((F opp) /. x) = (F9 /. x) opp by A43, Def3;

hence F9 /. x = (k opp) (*) ((F /. x) opp) by A43, Def3

.= ((F /. x) (*) k) opp by A46, A48, A49, A47, OPPCAT_1:16

.= (F /. x) (*) k ;

:: thesis: verum