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);

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 :: thesis: for x being set st x in I holds

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

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

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

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