let F1, F2 be covariant Functor of A,B; :: thesis: ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st
for a being Object of A holds t ! a is iso implies ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being Object of A holds t ! a is iso ) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1 ; :: thesis: ( for t being natural_transformation of F1,F2 holds
not for a being Object of A holds t ! a is iso or ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being Object of A holds t ! a is iso ) )
given t being natural_transformation of F1,F2 such that A3: for a being Object of A holds t ! a is iso ; :: thesis: ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being Object of A holds t ! a is iso )
consider f being natural_transformation of F2,F1 such that
A4: for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso ) by A1, A2, A3, Th32;
thus F2 is_naturally_transformable_to F1 by A1, A2, A3, Th32; :: thesis: ( F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being Object of A holds t ! a is iso )
thus F1 is_transformable_to F2 by A1; :: thesis: ex t being natural_transformation of F2,F1 st
for a being Object of A holds t ! a is iso
take f ; :: thesis: for a being Object of A holds f ! a is iso
thus for a being Object of A holds f ! a is iso by A4; :: thesis: verum