let C be Category; :: thesis: Obj (id C) = id the carrier of C
( dom (Obj (id C)) = the carrier of C & ( for x being object st x in the carrier of C holds
(Obj (id C)) . x = x ) ) by Th72, FUNCT_2:def 1;
hence Obj (id C) = id the carrier of C by FUNCT_1:17; :: thesis: verum