set S = the Functor of C opp ,D;

take /* the Functor of C opp ,D ; :: thesis: ( ( for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d ) & ( for f being Morphism of C holds

( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) )

thus for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d by Lm6; :: thesis: ( ( for f being Morphism of C holds

( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) )

thus for f being Morphism of C holds

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

(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g)

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) )

assume A1: dom g = cod f ; :: thesis: (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . 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 (/* the Functor of C opp ,D) . (gg (*) ff) = ((/* the Functor of C opp ,D) . ff) (*) ((/* the Functor of C opp ,D) . gg) by A1, Lm9;

hence (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ; :: thesis: verum

take /* the Functor of C opp ,D ; :: thesis: ( ( for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d ) & ( for f being Morphism of C holds

( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) )

thus for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d by Lm6; :: thesis: ( ( for f being Morphism of C holds

( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) )

thus for f being Morphism of C holds

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

(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g)

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) )

assume A1: dom g = cod f ; :: thesis: (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . 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 (/* the Functor of C opp ,D) . (gg (*) ff) = ((/* the Functor of C opp ,D) . ff) (*) ((/* the Functor of C opp ,D) . gg) by A1, Lm9;

hence (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ; :: thesis: verum