id a in Hom (a,a) by Th55;
hence id a is Morphism of a,a by Def7; :: thesis: verum