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

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

hence
opp (F opp) = F
by Th1; :: thesis: verum(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;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