let C be Category; :: thesis: id C is isomorphic
rng (id the carrier of C) = the carrier of C by RELAT_1:45;
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:45; :: according to CAT_1:def 19 :: thesis: verum