let F be Functor of A,B; :: thesis: ( F is_naturally_transformable_to F & ex t being natural_transformation of F,F st t is invertible )
thus F is_naturally_transformable_to F ; :: thesis: ex t being natural_transformation of F,F st t is invertible
take id F ; :: thesis: id F is invertible
let a be Object of A; :: according to NATTRA_1:def 10 :: thesis: (id F) . a is invertible
(id F) . a = id (F . a) by Th16;
hence (id F) . a is invertible by CAT_1:44; :: thesis: verum