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 CAT_1:4, A1;
( 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