let I be set ; :: thesis: for C being Category
for F being Function of I, the carrier' of C holds opp (F opp) = F
let C be Category; :: thesis: for F being Function of I, the carrier' of C holds opp (F opp) = F
let F be Function of I, the carrier' of C; :: thesis: opp (F opp) = F

now :: thesis: for x being set st x in I holds
(opp (F opp)) /. x = F /. x

let x be set ; :: thesis: ( x in I implies (opp (F opp)) /. x = F /. x )
assume A1: x in I ; :: thesis: (opp (F opp)) /. x = F /. x
hence (opp (F opp)) /. x = opp ((F opp) /. x) by Def4
.= opp ((F /. x) opp) by A1, Def3
.= F /. x ;
:: thesis: verum

end;

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