let A be Category; :: thesis: ex F being Functor of A,A st F is isomorphic
id A is isomorphic by CAT_1:122;
hence ex F being Functor of A,A st F is isomorphic ; :: thesis: verum