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