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

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

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

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

proof

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

end;

let f, g be Morphism of C; :: 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)
then A2: dom (S . f) = cod (S . g) by Th31;
reconsider Sff = S . f as Morphism of dom (S . f), cod (S . f) by CAT_1:4;
reconsider Sgg = S . g as Morphism of dom (S . g), cod (S . g) by CAT_1:4;
A3: ( Hom ((dom (S . f)),(cod (S . f))) <> {} & Hom ((dom (S . g)),(cod (S . g))) <> {} ) by CAT_1:2;
then A4: Sff opp = (S . f) opp by Def6;
A5: Sgg opp = (S . g) opp by A3, Def6;
thus (S *') . (g (*) f) = (S . (g (*) f)) opp by Def11
.= (Sff (*) Sgg) opp by A1, Def9
.= (Sgg opp) (*) (Sff opp) by A3, A2, Th14
.= ((S *') . g) (*) ((S . f) opp) by Def11, A4, A5
.= ((S *') . g) (*) ((S *') . f) by Def11 ; :: thesis: verum

end;

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