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