let B, C, D be Category; :: thesis: for S1 being Contravariant_Functor of C,B

for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

let S1 be Contravariant_Functor of C,B; :: thesis: for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

let S2 be Functor of B,D; :: thesis: S2 * S1 is Contravariant_Functor of C,D

*' S1 is Functor of C opp ,B by Th53;

then S2 * (*' S1) is Functor of C opp ,D by CAT_1:73;

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; :: thesis: verum

for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

let S1 be Contravariant_Functor of C,B; :: thesis: for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

let S2 be Functor of B,D; :: thesis: S2 * S1 is Contravariant_Functor of C,D

*' S1 is Functor of C opp ,B by Th53;

then S2 * (*' S1) is Functor of C opp ,D by CAT_1:73;

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; :: thesis: verum