let C, D be Category; for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D
let S be Functor of C,D; *' S is Contravariant_Functor of C opp ,D
thus
for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d
OPPCAT_1:def 9 ( ( for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) ) )
thus
for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) )
for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g)
let f, g be Morphism of (C opp); ( dom g = cod f implies (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) )
assume A1:
dom g = cod f
; (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g)
A2:
( dom (opp f) = cod f & cod (opp g) = dom g )
;
thus (*' S) . (g (*) f) =
S . (opp (g (*) f))
by Def10
.=
S . ((opp f) (*) (opp g))
by A1, Th16
.=
(S . (opp f)) (*) (S . (opp g))
by A1, A2, CAT_1:64
.=
((*' S) . f) (*) (S . (opp g))
by Def10
.=
((*' S) . f) (*) ((*' S) . g)
by Def10
; verum