let I be set ; for C being Category
for F being Function of I, the carrier' of C holds (F opp) opp = F
let C be Category; 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; (F opp) opp = F
now
(
C opp = CatStr(# the
carrier of
C, the
carrier' of
C, the
Target of
C, the
Source of
C,
(~ the Comp of C), the
Id of
C #) &
(C opp) opp = CatStr(# the
carrier of
(C opp), the
carrier' of
(C opp), the
Target of
(C opp), the
Source of
(C opp),
(~ the Comp of (C opp)), the
Id of
(C opp) #) )
by OPPCAT_1:def 1;
hence
the
carrier' of
C = the
carrier' of
((C opp) opp)
;
for x being set st x in I holds
((F opp) opp) /. x = F /. xlet x be
set ;
( x in I implies ((F opp) opp) /. x = F /. x )assume A1:
x in I
;
((F opp) opp) /. x = F /. xhence ((F opp) opp) /. x =
((F opp) /. x) opp
by Def5
.=
((F /. x) opp) opp
by A1, Def5
.=
F /. x
by OPPCAT_1:5
;
verum
hence
(F opp) opp = F
by Th1; verum