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

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 Lm16;
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 Lm16
.= id (dom ((*' S) . f)) by Lm17 ; :: thesis: (*' S) . (id (cod f)) = id (cod ((*' S) . f))
thus (*' S) . (id (cod f)) = id ((Obj (*' S)) . (cod f)) by Lm16
.= id (cod ((*' S) . f)) by Lm17 ; :: 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 Def8
.= S . ((opp f) * (opp g)) by A1, Th19
.= (S . (opp g)) * (S . (opp f)) by A1, A2, Def7
.= ((*' S) . g) * (S . (opp f)) by Def8
.= ((*' S) . g) * ((*' S) . f) by Def8 ; :: thesis: verum

end;

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