let C, D be Category; :: thesis: for S being Functor of C,D holds S *' is Contravariant_Functor of C,D opp
let S be Functor of C,D; :: thesis: S *' is Contravariant_Functor of C,D opp
thus for c being Object of C ex d being Object of (D opp ) st (S *' ) . (id c) = id d :: according to OPPCAT_1:def 7 :: thesis: ( ( for f being Morphism of C holds
( (S *' ) . (id (dom f)) = id (cod ((S *' ) . f)) & (S *' ) . (id (cod f)) = id (dom ((S *' ) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(S *' ) . (g * f) = ((S *' ) . f) * ((S *' ) . g) ) )

proof

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

end;

thus for f being Morphism of C 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 st dom g = cod f holds
(S *' ) . (g * f) = ((S *' ) . f) * ((S *' ) . g)

proof

let f be Morphism of C; :: 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 Lm22
.= id (cod ((S *' ) . f)) by Lm23 ; :: thesis: (S *' ) . (id (cod f)) = id (dom ((S *' ) . f))
thus (S *' ) . (id (cod f)) = id ((Obj (S *' )) . (cod f)) by Lm22
.= id (dom ((S *' ) . f)) by Lm23 ; :: thesis: verum

end;

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