let I be set ; :: thesis: for C being Category
for f being Morphism of C
for F being Projections_family of cod f,I holds (f opp) * (F opp) = (F * f) opp

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

let f be Morphism of C; :: thesis: for F being Projections_family of cod f,I holds (f opp) * (F opp) = (F * f) opp
let F be Projections_family of cod 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
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: dom (F /. x) = (doms F) /. x by Def1
.= (I --> (cod f)) /. x by Def13
.= cod f by ;
reconsider ff = f as Morphism of dom f, cod f by CAT_1:4;
reconsider gg = F /. x as Morphism of cod f, cod (F /. x) by ;
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 ;
thus ((f opp) * (F opp)) /. x = (f opp) (*) ((F opp) /. x) by
.= (f opp) (*) ((F /. x) opp) by
.= (gg (*) ff) opp by
.= ((F * f) /. x) opp by
.= ((F * f) opp) /. x by ; :: thesis: verum
end;
hence (f opp) * (F opp) = (F * f) opp by Th1; :: thesis: verum