let C be Category; :: thesis: id C is isomorphic
( rng (id the carrier' of C) = the carrier' of C & rng (id the carrier of C) = the carrier of C & id the carrier' of C is one-to-one ) 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; :: according to CAT_1:def 22 :: thesis: verum