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