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

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 Def6
.= opp ((F /. x) opp ) by A1, Def5
.= F /. x by OPPCAT_1:7 ;
:: thesis: verum

end;

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