theorem :: OPPCAT_1:53

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