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

now

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

end;

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

end;

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

now

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

end;

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