let I be set ; :: thesis: for C being Category

for f being Morphism of C

for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

let C be Category; :: thesis: for f being Morphism of C

for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

let f be Morphism of C; :: thesis: for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

let F be Injections_family of dom f,I; :: thesis: (F opp) * (f opp) = (f * F) opp

for f being Morphism of C

for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

let C be Category; :: thesis: for f being Morphism of C

for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

let f be Morphism of C; :: thesis: for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

let F be Injections_family of dom f,I; :: thesis: (F opp) * (f opp) = (f * F) opp

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

((F opp) * (f opp)) /. x = ((f * F) opp) /. x

hence
(F opp) * (f opp) = (f * F) opp
by Th1; :: thesis: verum((F opp) * (f opp)) /. x = ((f * F) opp) /. x

let x be set ; :: thesis: ( x in I implies ((F opp) * (f opp)) /. x = ((f * F) opp) /. x )

assume A1: x in I ; :: thesis: ((F opp) * (f opp)) /. x = ((f * F) opp) /. x

then A2: cod (F /. x) = (cods F) /. x by Def2

.= (I --> (dom f)) /. x by Def16

.= dom f by A1, Th2 ;

reconsider ff = f as Morphism of dom f, cod f by CAT_1:4;

reconsider gg = F /. x as Morphism of dom (F /. x), dom f by A2, CAT_1:4;

A3: ( Hom ((dom f),(cod f)) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A4: ff opp = f opp by OPPCAT_1:def 6;

A5: gg opp = (F /. x) opp by A3, A2, OPPCAT_1:def 6;

thus ((F opp) * (f opp)) /. x = ((F opp) /. x) (*) (f opp) by A1, Def5

.= ((F /. x) opp) (*) (f opp) by A1, Def3

.= (f (*) (F /. x)) opp by A2, A4, A5, A3, OPPCAT_1:16

.= ((f * F) /. x) opp by A1, Def6

.= ((f * F) opp) /. x by A1, Def3 ; :: thesis: verum

end;assume A1: x in I ; :: thesis: ((F opp) * (f opp)) /. x = ((f * F) opp) /. x

then A2: cod (F /. x) = (cods F) /. x by Def2

.= (I --> (dom f)) /. x by Def16

.= dom f by A1, Th2 ;

reconsider ff = f as Morphism of dom f, cod f by CAT_1:4;

reconsider gg = F /. x as Morphism of dom (F /. x), dom f by A2, CAT_1:4;

A3: ( Hom ((dom f),(cod f)) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} ) by CAT_1:2;

then A4: ff opp = f opp by OPPCAT_1:def 6;

A5: gg opp = (F /. x) opp by A3, A2, OPPCAT_1:def 6;

thus ((F opp) * (f opp)) /. x = ((F opp) /. x) (*) (f opp) by A1, Def5

.= ((F /. x) opp) (*) (f opp) by A1, Def3

.= (f (*) (F /. x)) opp by A2, A4, A5, A3, OPPCAT_1:16

.= ((f * F) /. x) opp by A1, Def6

.= ((f * F) opp) /. x by A1, Def3 ; :: thesis: verum