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