id a in Hom (a,a) by Def4;
hence dom (id a) = a by Th1; :: thesis: verum