theorem :: OPPCAT_1:50

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