let C, B be Category; :: thesis: for S being Functor of C opp ,B holds /* S is Contravariant_Functor of C,B
let S be Functor of C opp ,B; :: thesis: /* S is Contravariant_Functor of C,B
thus for c being Object of C ex d being Object of B st (/* S) . (id c) = id d by Lm3; :: according to OPPCAT_1:def 7 :: thesis: ( ( 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 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 Lm5, Lm6; :: thesis: verum