set S = the Functor of C opp ,D;
take
/* the Functor of C opp ,D
; ( ( 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; ( ( 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; 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; ( 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
; (/* 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)
; verum