let I be set ; :: thesis: for C being Category
for f being Morphism of C holds (I --> f) opp = I --> (f opp )
let C be Category; :: thesis: for f being Morphism of C holds (I --> f) opp = I --> (f opp )
let f be Morphism of C; :: thesis: (I --> f) opp = I --> (f opp )
set F = I --> f;
set F9 = I --> (f opp );

now

let x be set ; :: thesis: ( x in I implies ((I --> f) opp ) /. x = (I --> (f opp )) /. x )
assume A1: x in I ; :: thesis: ((I --> f) opp ) /. x = (I --> (f opp )) /. x
then ( (I --> f) /. x = f & (I --> (f opp )) /. x = f opp ) by Th2;
hence ((I --> f) opp ) /. x = (I --> (f opp )) /. x by A1, Def5; :: thesis: verum

end;

hence (I --> f) opp = I --> (f opp ) by Th1; :: thesis: verum