theorem Th33: :: ISOCAT_1:35

for A, B being Category
for F1, F2 being Functor of A,B
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id B) * s = s