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