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