Weyl Kac specializes to the finite Weyl character formula

By F4 the root set is finite and all its roots are real, so F3 gives multiplicity one. Weyl transformations permute the real roots. This permutation action is faithful: the finite-type Cartan matrix is nonsingular, so in its minimal realization the independent simple roots are a basis of the dual Cartan, and a linear map fixing every root fixes that basis. Thus $W$ embeds in the permutation group of a finite set and is finite.

Substitute the multiplicities of step 1.1 into F1. Its infinite-index notation is now the finite sum and finite product displayed above. The semisimple algebra, Cartan, simple coroot labels and positive generators coincide under F2's generator identification, so the simple highest-weight module and dominance convention are the same. This is the finite Weyl character formula with that positive Borel. The quotient denotes the equality after multiplication by its denominator, or the formal inverse used in F1; no division by a numerically zero specialization is made. Disconnected finite types are included by F2, and empty data give one monomial. No choice beyond finite linear algebra enters.