Free Lie construction for finite Kac Moody generators

Evaluate a formal bracket recursively under any linear map $V\to L$. Bilinearity, antisymmetry and Jacobi vanish on evaluation because they hold in $L$. Thus evaluation factors uniquely through a Lie homomorphism $F(V)\to L$. The quotient itself has an antisymmetric bilinear bracket satisfying Jacobi by its defining relations. Bracket words form a countable spanning list, so first independent words supply a basis.

The linear inclusion $V\to U(F(V))$ gives an associative map $T(V)\to U(F(V))$. Conversely step 1.1 applied to the commutator Lie algebra of $T(V)$ gives $F(V)\to T(V)$, hence an associative map $U(F(V))\to T(V)$ by the tensor-quotient relations. Both composites fix $V$. The algebra $T(V)$ is generated by $V$; $U(F(V))$ is also generated by $V$ because each bracket word is an associative commutator polynomial. Therefore the composites are identities.

PBW for the basis selected in step 1.1 injects $F(V)$ into $U(F(V))$. Composing with the isomorphism of step 2.1 proves injectivity into $T(V)$. Every element of its image is a linear combination of bracket words, and every such word is in the image, proving the image description.