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

proof

assume A1: cods F = I --> c ; :: according to CAT_3:def 16 :: thesis: opp F is Projections_family of opp c,I

now :: thesis: for x being set st x in I holds
(doms (opp F)) /. x = (I --> (opp c)) /. x

let x be set ; :: thesis: ( x in I implies (doms (opp F)) /. x = (I --> (opp c)) /. x )
reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;
A2: Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;
assume A3: x in I ; :: thesis: (doms (opp F)) /. x = (I --> (opp c)) /. x
hence (doms (opp F)) /. x = dom ((opp F) /. x) by Def1
.= dom (opp (F /. x)) by A3, Def4
.= opp (cod (F /. x)) by A2, OPPCAT_1:13
.= (I --> (opp c)) /. x by A1, A3, Def2 ;
:: thesis: verum

end;

hence doms (opp F) = I --> (opp c) by Th1; :: according to CAT_3:def 13 :: thesis: verum

end;

assume A4: doms (opp F) = I --> (opp c) ; :: according to CAT_3:def 13 :: thesis: F is Injections_family of c,I

now :: thesis: for x being set st x in I holds
(cods F) /. x = (I --> c) /. x

let x be set ; :: thesis: ( x in I implies (cods F) /. x = (I --> c) /. x )
reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;
Hom ((dom gg),(cod gg)) <> {} by CAT_1:2;
then A5: gg opp = (F /. x) opp by OPPCAT_1:def 6;
assume A6: x in I ; :: thesis: (cods F) /. x = (I --> c) /. x
hence (cods F) /. x = cod (F /. x) by Def2
.= dom (opp (F /. x)) by A5, OPPCAT_1:11
.= dom ((opp F) /. x) by A6, Def4
.= (I --> c) /. x by A4, A6, Def1 ;
:: thesis: verum

end;

hence cods F = I --> c by Th1; :: according to CAT_3:def 16 :: thesis: verum