[proofplan]We compare the given semisimple Lie algebra with the abstract Lie algebra defined by the same generators and relations. The Cartan and Serre relations give a canonical surjective homomorphism from the Serre-presented Lie algebra onto the semisimple Lie algebra. The finite-type Serre construction theorem identifies the abstract quotient as the unique split semisimple Lie algebra with Cartan matrix $A$, so the canonical homomorphism is also injective. This proves that the listed generators and relations present the associated semisimple Lie algebra.[/proofplan]

[step:Construct the Serre-presented Lie algebra] Let $\mathfrak{s}(A)$ denote the Lie algebra generated by symbols $E_i$, $F_i$, and $H_i$ for $1 \le i \le l$, modulo the ideal generated by the Cartan relations \begin{align*} [H_i,H_j]&=0, & [H_i,E_j]&=a_{ij}E_j, & [H_i,F_j]&=-a_{ij}F_j, & [E_i,F_j]&=\delta_{ij}H_i, \end{align*} and the Serre relations \begin{align*} (\operatorname{ad}_{E_i})^{1-a_{ij}}(E_j)&=0, & (\operatorname{ad}_{F_i})^{1-a_{ij}}(F_j)&=0 \end{align*} for $i\neq j$. Here $\operatorname{ad}_X: \mathfrak{s}(A) \to \mathfrak{s}(A)$ is the adjoint map $Y \mapsto [X,Y]$. [/step]

[step:Define the canonical homomorphism onto the associated semisimple Lie algebra]Let $\mathfrak{g}$ be the semisimple Lie algebra associated to the finite-type Cartan matrix $A$, with Chevalley generators $e_i$, $f_i$, and $h_i$ for $1\le i\le l$. These elements satisfy exactly the Cartan and Serre relations in the statement. Therefore the universal property of the quotient defining $\mathfrak{s}(A)$ gives a unique Lie algebra homomorphism \begin{align*} \Phi: \mathfrak{s}(A) &\to \mathfrak{g}, & E_i &\mapsto e_i, & F_i &\mapsto f_i, & H_i &\mapsto h_i. \end{align*} Since $\mathfrak{g}$ is generated by the elements $e_i$, $f_i$, and $h_i$, the map $\Phi$ is surjective.[/step]

[guided]The point of introducing $\mathfrak{s}(A)$ is that it is the largest Lie algebra in which the displayed relations hold. Because the Chevalley generators $e_i$, $f_i$, and $h_i$ in $\mathfrak{g}$ satisfy those same relations, the assignment \begin{align*} E_i &\mapsto e_i, & F_i &\mapsto f_i, & H_i &\mapsto h_i \end{align*} respects every generator of the defining ideal of $\mathfrak{s}(A)$. Hence it descends from the free Lie algebra to the quotient $\mathfrak{s}(A)$ and defines a Lie algebra homomorphism $\Phi: \mathfrak{s}(A) \to \mathfrak{g}$. The image of $\Phi$ contains each generator $e_i$, $f_i$, and $h_i$ of $\mathfrak{g}$, so the image is all of $\mathfrak{g}$. Thus $\Phi$ is surjective.[/guided]

[step:Apply the finite-type Serre construction theorem to identify the abstract quotient]Because $A$ is a Cartan matrix of finite type, the finite-type Serre construction theorem applies to $\mathfrak{s}(A)$. It states that $\mathfrak{s}(A)$ is finite-dimensional and semisimple, that the subalgebra $\mathfrak{h}_{A}:=\operatorname{span}\{H_1,\dots,H_l\}$ is a Cartan subalgebra, and that the Cartan matrix of $\mathfrak{s}(A)$ with respect to the simple root vectors $E_i,F_i$ is precisely $A$. The theorem applies here because the defining matrix is assumed to be a finite-type Cartan matrix, and $\mathfrak{s}(A)$ was defined by imposing exactly the Cartan and Serre relations required in the construction theorem.[/step]

[guided]We now use the structural theorem that is specific to finite type. It says that if a matrix $A$ is a finite-type Cartan matrix and one forms the Lie algebra from generators $E_i,F_i,H_i$ subject to the Cartan and Serre relations, then the resulting Lie algebra is not merely a formal quotient: it is a finite-dimensional semisimple Lie algebra. Its Cartan subalgebra is \begin{align*} \mathfrak{h}_{A}:=\operatorname{span}\{H_1,\dots,H_l\}, \end{align*} and its simple root data has Cartan matrix $A$. The hypotheses are exactly those available in the theorem statement: $A$ is finite type, and $\mathfrak{s}(A)$ was constructed from the corresponding Serre relations. This is where finite type is used. Without finite type, the same presentation generally produces a Kac-Moody algebra rather than a finite-dimensional semisimple Lie algebra.[/guided]

[step:Use uniqueness of the semisimple Lie algebra with Cartan matrix $A$]The classification and uniqueness theorem for finite-dimensional semisimple Lie algebras says that two semisimple Lie algebras with the same finite-type Cartan matrix are isomorphic by an isomorphism carrying the corresponding Chevalley generators to one another. Applying this to $\mathfrak{s}(A)$ and $\mathfrak{g}$ shows that the surjective homomorphism $\Phi$ is an isomorphism.[/step]

[guided]At this point both Lie algebras have the same root-theoretic data. The abstract algebra $\mathfrak{s}(A)$ is semisimple with Cartan matrix $A$, and the given algebra $\mathfrak{g}$ is, by definition, the semisimple Lie algebra associated to the same finite-type Cartan matrix $A$. The finite-type classification theorem identifies semisimple Lie algebras by their Cartan matrices, with the Chevalley generators corresponding under the identification. Therefore the homomorphism $\Phi: \mathfrak{s}(A) \to \mathfrak{g}$ cannot have a nonzero kernel: a nonzero kernel would make $\mathfrak{g}$ a proper quotient of the semisimple Lie algebra with the same root datum, contradicting uniqueness of the semisimple Lie algebra associated to $A$. Since $\Phi$ was already shown to be surjective, injectivity makes $\Phi$ an isomorphism.[/guided]

[step:Conclude that the displayed relations give the presentation] Since $\Phi: \mathfrak{s}(A) \to \mathfrak{g}$ is an isomorphism and sends $E_i$, $F_i$, and $H_i$ to $e_i$, $f_i$, and $h_i$, respectively, the Lie algebra $\mathfrak{g}$ is generated by $e_i$, $f_i$, and $h_i$ subject only to the displayed Cartan and Serre relations. This is exactly the claimed Serre presentation. [/step]