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

now

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

end;

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