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 )

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

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

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

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

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

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

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