theorem Th20: :: FUNCTOR3:20

for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(id B) * p = p