let B, C, D be Category; for S1 being Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
let S1 be Functor of C,B; for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
let S2 be Contravariant_Functor of B,D; S2 * S1 is Contravariant_Functor of C,D
*' S1 is Contravariant_Functor of C opp ,B
by Th55;
then
S2 * (*' S1) is Functor of C opp ,D
by Th33;
then
/* (S2 * (*' S1)) is Contravariant_Functor of C,D
by Th32;
then
S2 * (/* (*' S1)) is Contravariant_Functor of C,D
by Lm18;
hence
S2 * S1 is Contravariant_Functor of C,D
by Th45; verum