let A, B be Category; :: thesis: for F being Functor of A,B holds id F is natural_equivalence of F,F
let F be Functor of A,B; :: thesis: id F is natural_equivalence of F,F
thus F ~= F ; :: according to NATTRA_1:def 14 :: 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