theorem Th32: :: FUNCTOR3:32

for A, B being category
for F1, F2 being covariant Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being Object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso ) )