let F be covariant Functor of A,B; :: thesis: ( F is_naturally_transformable_to F & F is_transformable_to F & ex t being natural_transformation of F,F st

for a being Object of A holds t ! a is iso )

thus ( F is_naturally_transformable_to F & F is_transformable_to F ) ; :: thesis: ex t being natural_transformation of F,F st

for a being Object of A holds t ! a is iso

take idt F ; :: thesis: for a being Object of A holds (idt F) ! a is iso

let a be Object of A; :: thesis: (idt F) ! a is iso

(idt F) ! a = idm (F . a) by FUNCTOR2:4;

hence (idt F) ! a is iso ; :: thesis: verum

for a being Object of A holds t ! a is iso )

thus ( F is_naturally_transformable_to F & F is_transformable_to F ) ; :: thesis: ex t being natural_transformation of F,F st

for a being Object of A holds t ! a is iso

take idt F ; :: thesis: for a being Object of A holds (idt F) ! a is iso

let a be Object of A; :: thesis: (idt F) ! a is iso

(idt F) ! a = idm (F . a) by FUNCTOR2:4;

hence (idt F) ! a is iso ; :: thesis: verum