theorem :: OPPCAT_1:52

for B, C, D being Category
for S being Function of the carrier' of C, the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S)