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

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 Def3
.= (I --> (cod f)) /. x by Def14
.= cod f by A1, Th2 ;
thus ((f opp ) * (F opp )) /. x = (f opp ) * ((F opp ) /. x) by A1, Def8
.= (f opp ) * ((F /. x) opp ) by A1, Def5
.= ((F /. x) * f) opp by A2, OPPCAT_1:17
.= ((F * f) /. x) opp by A1, Def7
.= ((F * f) opp ) /. x by A1, Def5 ; :: thesis: verum

end;

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