theorem :: OPPCAT_1:49

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