theorem :: CAT_2:38

for C, D, C9 being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9
for f being Morphism of C holds (S -? c9) . f = S . (f,(id c9)) by FUNCT_5:70;