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