theorem :: OPPCAT_1:51

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