let I be set ; :: thesis: for C being Category

for F being Function of I, the carrier' of C holds (F opp) opp = F

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

let F be Function of I, the carrier' of C; :: thesis: (F opp) opp = F

for F being Function of I, the carrier' of C holds (F opp) opp = F

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

let F be Function of I, the carrier' of C; :: thesis: (F opp) opp = F

now :: thesis: ( the carrier' of C = the carrier' of ((C opp) opp) & ( for x being set st x in I holds

((F opp) opp) /. x = F /. x ) )

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

thus
the carrier' of C = the carrier' of ((C opp) opp)
; :: thesis: for x being set st x in I holds

((F opp) opp) /. x = F /. x

let x be set ; :: thesis: ( x in I implies ((F opp) opp) /. x = F /. x )

assume A1: x in I ; :: thesis: ((F opp) opp) /. x = F /. x

hence ((F opp) opp) /. x = ((F opp) /. x) opp by Def3

.= ((F /. x) opp) opp by A1, Def3

.= F /. x ;

:: thesis: verum

end;((F opp) opp) /. x = F /. x

let x be set ; :: thesis: ( x in I implies ((F opp) opp) /. x = F /. x )

assume A1: x in I ; :: thesis: ((F opp) opp) /. x = F /. x

hence ((F opp) opp) /. x = ((F opp) /. x) opp by Def3

.= ((F /. x) opp) opp by A1, Def3

.= F /. x ;

:: thesis: verum