let C, D be Category; :: thesis: for S being Contravariant_Functor of C,D holds *' S is Functor of C opp ,D
let S be Contravariant_Functor of C,D; :: thesis: *' S is Functor of C opp ,D

now :: thesis: ( ( for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d ) & ( for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) ) )

thus for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d :: thesis: ( ( for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) ) )

proof

let c be Object of (C opp); :: thesis: ex d being Object of D st (*' S) . (id c) = id d
(*' S) . (id c) = id ((Obj (*' S)) . c) by Lm19;
hence ex d being Object of D st (*' S) . (id c) = id d ; :: thesis: verum

end;

thus for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) :: thesis: for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f)

proof

let f be Morphism of (C opp); :: thesis: ( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) )
thus (*' S) . (id (dom f)) = id ((Obj (*' S)) . (dom f)) by Lm19
.= id (dom ((*' S) . f)) by Lm20 ; :: thesis: (*' S) . (id (cod f)) = id (cod ((*' S) . f))
thus (*' S) . (id (cod f)) = id ((Obj (*' S)) . (cod f)) by Lm19
.= id (cod ((*' S) . f)) by Lm20 ; :: thesis: verum

end;

let f, g be Morphism of (C opp); :: thesis: ( dom g = cod f implies (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) )
assume A1: dom g = cod f ; :: thesis: (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f)
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 g)) (*) (S . (opp f)) by A1, A2, Def9
.= ((*' S) . g) (*) (S . (opp f)) by Def10
.= ((*' S) . g) (*) ((*' S) . f) by Def10 ; :: thesis: verum

end;

hence *' S is Functor of C opp ,D by CAT_1:61; :: thesis: verum