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 F9 = I --> (opp f);

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 F9 = I --> (opp f);

now :: thesis: for x being set st x in I holds

(opp (I --> f)) /. x = (I --> (opp f)) /. x

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

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, Def4; :: thesis: verum

end;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, Def4; :: thesis: verum