consider S being Functor of C opp ,D;
take /* S ; :: thesis: ( ( for c being Object of C ex d being Object of D st (/* S) . (id c) = id d ) & ( 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 c being Object of C ex d being Object of D st (/* S) . (id c) = id d ) & ( 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) ) ) by Lm3, Lm5, Lm6; :: thesis: verum