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