theorem Th5: :: FUNCTOR2:5

for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )