let B, C 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 Lm6; :: according to OPPCAT_1:def 9 :: 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)) ) by Lm8; :: thesis: for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) )
assume A1: dom g = cod f ; :: thesis: (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . 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 (/* S) . (gg (*) ff) = ((/* S) . ff) (*) ((/* S) . gg) by A1, Lm9;
hence (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ; :: thesis: verum