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 ) & ( 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) ) ) by Lm3, Lm5, Lm6; :: thesis: verum