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 14 :: thesis: F opp is Injections_family of c opp ,I

now

let x be set ; :: thesis: ( x in I implies (cods (F opp )) /. x = (I --> (c opp )) /. x )
assume A2: x in I ; :: thesis: (cods (F opp )) /. x = (I --> (c opp )) /. x
hence (cods (F opp )) /. x = cod ((F opp ) /. x) by Def4
.= cod ((F /. x) opp ) by A2, Def5
.= (dom (F /. x)) opp by OPPCAT_1:11
.= ((I --> c) /. x) opp by A1, A2, Def3
.= c opp by A2, Th2
.= (I --> (c opp )) /. x by A2, Th2 ;
:: thesis: verum

end;

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

end;

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

now

let x be set ; :: thesis: ( x in I implies (doms F) /. x = (I --> c) /. x )
assume A4: x in I ; :: thesis: (doms F) /. x = (I --> c) /. x
hence (doms F) /. x = dom (F /. x) by Def3
.= cod ((F /. x) opp ) by OPPCAT_1:9
.= cod ((F opp ) /. x) by A4, Def5
.= (I --> (c opp )) /. x by A3, A4, Def4
.= c opp by A4, Th2
.= c by OPPCAT_1:def 2
.= (I --> c) /. x by A4, Th2 ;
:: thesis: verum

end;

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