let C, B 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

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 Lm8;
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 Lm8
.= id (dom ((/* S) . f)) by Lm9 ; :: thesis: (/* S) . (id (cod f)) = id (cod ((/* S) . f))
thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm8
.= id (cod ((/* S) . f)) by Lm9 ; :: 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 ) ;
thus (/* S) . (g * f) = S . ((g * f) opp) by Def6
.= S . ((f opp) * (g opp)) by A1, Th17
.= (S . (g opp)) * (S . (f opp)) by A1, A2, Def7
.= ((/* S) . g) * (S . (f opp)) by Def6
.= ((/* S) . g) * ((/* S) . f) by Def6 ; :: thesis: verum

end;

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