theorem :: FUNCTOR2:9

for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t ) by Th5;