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

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

end;

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