theorem :: OPPCAT_1:54

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