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 )

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 A4:
doms (opp F) = I --> (opp c)
; :: according to CAT_3:def 13 :: thesis: F is Injections_family of c,I
assume A1:
cods F = I --> c
; :: according to CAT_3:def 16 :: thesis: opp F is Projections_family of opp c,I

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

(doms (opp F)) /. x = (I --> (opp c)) /. x

hence
doms (opp F) = I --> (opp c)
by Th1; :: according to CAT_3:def 13 :: thesis: verum(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;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

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

(cods F) /. x = (I --> c) /. x

hence
cods F = I --> c
by Th1; :: according to CAT_3:def 16 :: thesis: verum(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;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