original argument of Hermann Weyl. We continue to let be a connected compact Lie group and a fixed maximal torus in . We focus on the most difficult part of the theorem, showing that every dominant, analytically integral element is the highest weight of some (finite-dimensional) irreducible representation. The tools for the proof are the following: The torus theorem. The Weyl integral formula. The Peter–Weyl theorem for class functions, which states that the characters of the irreducible representations form an orthonormal basis for the space of square integrable class functions on . With these tools in hand, we proceed with the proof. The first major step in the argument is to prove the Weyl character formula. The formula states that if is an irreducible representation with highest weight , then the character of satisfies: for all in the Lie algebra of . Here is half the sum of the positive roots. (The notation uses the convention of "real weights"; this convention requires an explicit factor of in the exponent.) Weyl's proof of the character formula is analytic in nature and hinges on the fact that the norm of the character is 1. Specifically, if there were any additional terms in the numerator, the Weyl integral formula would force the norm of the character to be greater than 1. Next, we let denote the function on the right-hand side of the character formula. We show that even if is not known to be the highest weight of a representation, is a well-defined, Weyl-invariant function on , which therefore extends to a class function on . Then using the Weyl integral formula, one can show that as ranges over the set of dominant, analytically integral elements, the functions form an orthonormal family of class functions. We emphasize that we do not currently know that every such is the highest weight of a representation; nevertheless, the expressions on the right-hand side of the character formula gives a well-defined set of functions , and these functions are orthonormal. Now comes the conclusion. The set of all —with ranging over the dominant, analytically integral elements—forms an orthonormal set in the space of square integrable class functions. But by the Weyl character formula, the characters of the irreducible representations form a subset of the 's. And by the Peter–Weyl theorem, the characters of the irreducible representations form an orthonormal basis for the space of square integrable