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

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