let
C
,
D
be
Category
;
:: thesis:
for
F
being
Functor
of
C
,
D
holds
(
*'
F
)
*'
is
Functor
of
C
opp
,
D
opp
let
F
be
Functor
of
C
,
D
;
:: thesis:
(
*'
F
)
*'
is
Functor
of
C
opp
,
D
opp
*'
F
is
Contravariant_Functor
of
C
opp
,
D
by
Th55
;
hence
(
*'
F
)
*'
is
Functor
of
C
opp
,
D
opp
by
Th54
;
:: thesis:
verum