theorem Th45: :: OPPCAT_1:47

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