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

now :: thesis: ( ( for c being Object of C ex d being Object of B 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 B 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 B st (/* S) . (id c) = id d
(/* S) . (id c) = id ((Obj (/* S)) . c) by Lm11;
hence ex d being Object of B 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 Lm11
.= id (dom ((/* S) . f)) by Lm12 ; :: thesis: (/* S) . (id (cod f)) = id (cod ((/* S) . f))
thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm11
.= id (cod ((/* S) . f)) by Lm12 ; :: 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)
A2: ( dom (f opp) = cod f & cod (g opp) = dom g ) ;
reconsider ff = f as Morphism of dom f, cod f by CAT_1:4;
reconsider gg = g as Morphism of cod f, cod g by A1, CAT_1:4;
A3: ( Hom ((dom f),(cod f)) <> {} & Hom ((dom g),(cod g)) <> {} ) by CAT_1:2;
then A4: ff opp = f opp by Def6;
A5: gg opp = g opp by Def6, A3, A1;
thus (/* S) . (g (*) f) = S . ((g (*) f) opp) by Def8
.= S . ((f opp) (*) (g opp)) by A4, A5, A3, A1, Th14
.= (S . (g opp)) (*) (S . (f opp)) by A1, A2, Def9
.= ((/* S) . g) (*) (S . (f opp)) by Def8
.= ((/* S) . g) (*) ((/* S) . f) by Def8 ; :: thesis: verum

end;

hence /* S is Functor of C,B by CAT_1:61; :: thesis: verum