theorem Th15: :: ISOCAT_2:17

for A, B, C being Category
for F being Functor of [:A,B:],C
for f being Morphism of A
for b being Object of B holds (F ?- f) . b = F . (f,(id b))