let B, C, D be Category; for S1 being Contravariant_Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D
let S1 be Contravariant_Functor of C,B; for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D
let S2 be Contravariant_Functor of B,D; S2 * S1 is Functor of C,D
set T = S2 * S1;
hence
S2 * S1 is Functor of C,D
by CAT_1:61; verum