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

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

thus for c being Object of C ex d being Object of B st (/* S) . (id c) = id d by Lm6; :: according to OPPCAT_1:def 9 :: 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) ) )

thus for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) by Lm8; :: thesis: for f, g being Morphism of C st dom g = cod f holds

(/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

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)

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;

( Hom ((dom f),(cod f)) <> {} & Hom ((dom g),(cod g)) <> {} ) by CAT_1:2;

then (/* S) . (gg (*) ff) = ((/* S) . ff) (*) ((/* S) . gg) by A1, Lm9;

hence (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ; :: thesis: verum

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

thus for c being Object of C ex d being Object of B st (/* S) . (id c) = id d by Lm6; :: according to OPPCAT_1:def 9 :: 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) ) )

thus for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) by Lm8; :: thesis: for f, g being Morphism of C st dom g = cod f holds

(/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

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)

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;

( Hom ((dom f),(cod f)) <> {} & Hom ((dom g),(cod g)) <> {} ) by CAT_1:2;

then (/* S) . (gg (*) ff) = ((/* S) . ff) (*) ((/* S) . gg) by A1, Lm9;

hence (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ; :: thesis: verum