theorem Th23: :: ISOCAT_1:25

for A, B being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} by NATTRA_1:def 2;