let C, D be Category; :: thesis: for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D
let S be Functor of C,D; :: thesis: *' 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 :: according to OPPCAT_1:def 7 :: thesis: ( ( 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) ) )

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 Lm20;
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 (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) :: thesis: for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g * f) = ((*' S) . f) * ((*' S) . g)

proof

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

end;

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