theorem :: OPPCAT_1:69

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