let C be Category; :: thesis: id C is isomorphic
rng (id the carrier of C) = the carrier of C ;
hence ( id C is one-to-one & rng (id C) = the carrier' of C & rng (Obj (id C)) = the carrier of C ) by Th73; :: according to CAT_1:def 25 :: thesis: verum