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 ) by FUNCTOR2:9; :: 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:6;
hence (idt F) ! a is iso ; :: thesis: verum