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
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
let C be Category; :: thesis: for c being Object of C
for F being Function of I, the carrier' of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
let c be Object of C; :: thesis: for F being Function of I, the carrier' of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
let F be Function of I, the carrier' of C; :: thesis: ( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
thus ( F is Projections_family of c,I implies F opp is Injections_family of c opp ,I ) :: thesis: ( F opp is Injections_family of c opp ,I implies F is Projections_family of c,I )

proof

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

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

let x be set ; :: thesis: ( x in I implies (cods (F opp)) /. x = (I --> (c opp)) /. 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;
then A3: gg opp = (F /. x) opp by OPPCAT_1:def 6;
assume A4: x in I ; :: thesis: (cods (F opp)) /. x = (I --> (c opp)) /. x
hence (cods (F opp)) /. x = cod ((F opp) /. x) by Def2
.= cod ((F /. x) opp) by A4, Def3
.= (dom (F /. x)) opp by A2, A3, OPPCAT_1:12
.= (I --> (c opp)) /. x by A1, A4, Def1 ;
:: thesis: verum

end;

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

end;

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

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

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

end;

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