[proofplan]
We prove the result by induction on $\dim_F \mathfrak g$. If $\mathfrak g$ is already simple, the decomposition has one summand. Otherwise we choose a non-zero proper ideal $\mathfrak a \trianglelefteq \mathfrak g$ and use the orthogonal-complement decomposition theorem for ideals in a semisimple Lie algebra to split $\mathfrak g$ as a direct sum of two smaller commuting semisimple ideals. Applying the induction hypothesis to those two ideals and then viewing the resulting simple summands as ideals of $\mathfrak g$ gives the desired decomposition.
[/proofplan]
[step:Start the induction and dispose of the simple case]
We argue by induction on the integer $n := \dim_F \mathfrak g$.
If $n=0$, then $\mathfrak g=0$ and the assertion holds with $m=0$, where the right-hand side is the empty direct sum. If $n>0$ and $\mathfrak g$ is simple, then the assertion holds with $m=1$ and $\mathfrak g_1 := \mathfrak g$.
It remains to consider the case in which $\mathfrak g$ is non-zero, semisimple, and not simple. Then there exists a non-zero proper ideal $\mathfrak a \trianglelefteq \mathfrak g$.
[guided]
The induction parameter is the finite dimension
\begin{align*}
n := \dim_F \mathfrak g.
\end{align*}
This is well-defined because $\mathfrak g$ is finite-dimensional over $F$ by hypothesis.
There are two terminal cases. First, if $n=0$, then $\mathfrak g=0$. The statement allows $m=0$, and the empty direct sum is $0$, so the result holds.
Second, suppose $n>0$ and $\mathfrak g$ is simple. By definition, a simple Lie algebra is non-zero and has no non-zero proper ideals. In this case we take
\begin{align*}
m := 1,
\qquad
\mathfrak g_1 := \mathfrak g.
\end{align*}
Then $\mathfrak g_1$ is a simple ideal of $\mathfrak g$, and
\begin{align*}
\mathfrak g = \mathfrak g_1.
\end{align*}
There are no distinct indices $i,j$ to check for the commutation condition.
Thus the only remaining case is that $\mathfrak g$ is non-zero, semisimple, and not simple. Since it is not simple, there exists a non-zero proper ideal
\begin{align*}
\mathfrak a \trianglelefteq \mathfrak g,
\qquad
0 \neq \mathfrak a \neq \mathfrak g.
\end{align*}
This ideal is the object to which we apply the splitting theorem in the next step.
[/guided]
[/step]
[step:Split off a commuting semisimple complementary ideal]
Let $\kappa_{\mathfrak g}: \mathfrak g \times \mathfrak g \to F$ denote the Killing form of $\mathfrak g$, and define the orthogonal complement of $\mathfrak a$ in $\mathfrak g$ by
\begin{align*}
\mathfrak a^\perp
:=
\{x \in \mathfrak g : \kappa_{\mathfrak g}(x,y)=0 \text{ for every } y \in \mathfrak a\}.
\end{align*}
By the orthogonal-complement theorem for ideals in semisimple Lie algebras (citing a result not yet in the wiki: Orthogonal Complement Theorem for Ideals in Semisimple Lie Algebras), $\mathfrak a^\perp$ is an ideal of $\mathfrak g$ and
\begin{align*}
\mathfrak g = \mathfrak a \oplus \mathfrak a^\perp,
\qquad
[\mathfrak a,\mathfrak a^\perp]=0.
\end{align*}
Since $\mathfrak a$ is non-zero and proper, this direct-sum decomposition implies
\begin{align*}
0 < \dim_F \mathfrak a < \dim_F \mathfrak g,
\qquad
0 < \dim_F \mathfrak a^\perp < \dim_F \mathfrak g.
\end{align*}
[guided]
We use the Killing form to produce the complementary ideal. Let
\begin{align*}
\kappa_{\mathfrak g}: \mathfrak g \times \mathfrak g &\to F
\end{align*}
be the Killing form of $\mathfrak g$. For the chosen ideal $\mathfrak a \trianglelefteq \mathfrak g$, define its Killing-orthogonal complement by
\begin{align*}
\mathfrak a^\perp
:=
\{x \in \mathfrak g : \kappa_{\mathfrak g}(x,y)=0 \text{ for every } y \in \mathfrak a\}.
\end{align*}
The relevant structural input is the orthogonal-complement theorem for ideals in semisimple Lie algebras (citing a result not yet in the wiki: Orthogonal Complement Theorem for Ideals in Semisimple Lie Algebras). Its hypotheses are satisfied here: $F$ has characteristic $0$, $\mathfrak g$ is finite-dimensional and semisimple over $F$, and $\mathfrak a$ is an ideal of $\mathfrak g$. Therefore the theorem gives three conclusions:
\begin{align*}
\mathfrak a^\perp \trianglelefteq \mathfrak g,
\qquad
\mathfrak g = \mathfrak a \oplus \mathfrak a^\perp,
\qquad
[\mathfrak a,\mathfrak a^\perp]=0.
\end{align*}
The direct sum is crucial for induction because it makes both summands strictly smaller. Since $\mathfrak a \neq 0$, we have $\dim_F \mathfrak a>0$. Since $\mathfrak a \neq \mathfrak g$ and
\begin{align*}
\mathfrak g = \mathfrak a \oplus \mathfrak a^\perp,
\end{align*}
the complement $\mathfrak a^\perp$ is non-zero. Also both summands are proper subspaces of $\mathfrak g$, so
\begin{align*}
0 < \dim_F \mathfrak a < \dim_F \mathfrak g,
\qquad
0 < \dim_F \mathfrak a^\perp < \dim_F \mathfrak g.
\end{align*}
Thus both summands fall within the induction range.
[/guided]
[/step]
[step:Verify that both summands are semisimple]
We show that $\mathfrak a$ is semisimple; the same argument applies to $\mathfrak a^\perp$.
Let $\mathfrak r \trianglelefteq \mathfrak a$ be a solvable ideal of the Lie algebra $\mathfrak a$. For every $x \in \mathfrak g$, write uniquely
\begin{align*}
x = y + z,
\qquad
y \in \mathfrak a,
\qquad
z \in \mathfrak a^\perp.
\end{align*}
Since $\mathfrak r \trianglelefteq \mathfrak a$, we have $[y,\mathfrak r]\subseteq \mathfrak r$. Since $[\mathfrak a^\perp,\mathfrak a]=0$ and $\mathfrak r \subseteq \mathfrak a$, we have $[z,\mathfrak r]=0$. Therefore
\begin{align*}
[x,\mathfrak r]
=
[y+z,\mathfrak r]
\subseteq
[y,\mathfrak r]+[z,\mathfrak r]
\subseteq
\mathfrak r.
\end{align*}
Hence $\mathfrak r \trianglelefteq \mathfrak g$. Because $\mathfrak r$ is solvable and $\mathfrak g$ is semisimple, $\mathfrak r=0$. Thus $\mathfrak a$ has no non-zero solvable ideals, so $\mathfrak a$ is semisimple. The same proof with $\mathfrak a$ and $\mathfrak a^\perp$ interchanged shows that $\mathfrak a^\perp$ is semisimple.
[guided]
We now need to justify that induction applies not just dimensionally, but also structurally: the summands must themselves be semisimple Lie algebras.
We prove this for $\mathfrak a$. Let
\begin{align*}
\mathfrak r \trianglelefteq \mathfrak a
\end{align*}
be a solvable ideal of the Lie algebra $\mathfrak a$. To prove that $\mathfrak a$ is semisimple, we must show $\mathfrak r=0$.
The point is that $\mathfrak r$ is automatically an ideal of the larger Lie algebra $\mathfrak g$. Let $x \in \mathfrak g$. Since
\begin{align*}
\mathfrak g = \mathfrak a \oplus \mathfrak a^\perp,
\end{align*}
there exist unique elements $y \in \mathfrak a$ and $z \in \mathfrak a^\perp$ such that
\begin{align*}
x = y+z.
\end{align*}
Because $\mathfrak r$ is an ideal of $\mathfrak a$, the bracket of $y$ with $\mathfrak r$ stays inside $\mathfrak r$:
\begin{align*}
[y,\mathfrak r]\subseteq \mathfrak r.
\end{align*}
Because the two summands commute and $\mathfrak r \subseteq \mathfrak a$, we also have
\begin{align*}
[z,\mathfrak r]=0.
\end{align*}
Combining these two facts gives
\begin{align*}
[x,\mathfrak r]
=
[y+z,\mathfrak r]
\subseteq
[y,\mathfrak r]+[z,\mathfrak r]
\subseteq
\mathfrak r.
\end{align*}
Thus $\mathfrak r \trianglelefteq \mathfrak g$.
Now $\mathfrak r$ is a solvable ideal of $\mathfrak g$. Since $\mathfrak g$ is semisimple, it has no non-zero solvable ideals. Therefore $\mathfrak r=0$. This proves that $\mathfrak a$ is semisimple.
The same argument applies to $\mathfrak a^\perp$: if $\mathfrak s \trianglelefteq \mathfrak a^\perp$ is solvable, then the decomposition
\begin{align*}
\mathfrak g = \mathfrak a \oplus \mathfrak a^\perp
\end{align*}
and the commutation relation $[\mathfrak a,\mathfrak a^\perp]=0$ imply $\mathfrak s \trianglelefteq \mathfrak g$, hence $\mathfrak s=0$. Therefore $\mathfrak a^\perp$ is semisimple.
[/guided]
[/step]
[step:Apply induction to the two smaller semisimple ideals]
By the induction hypothesis applied to $\mathfrak a$, there exist simple ideals
\begin{align*}
\mathfrak a_1,\dots,\mathfrak a_p \trianglelefteq \mathfrak a
\end{align*}
such that
\begin{align*}
\mathfrak a = \mathfrak a_1 \oplus \cdots \oplus \mathfrak a_p,
\qquad
[\mathfrak a_i,\mathfrak a_j]=0 \quad \text{for } i\neq j.
\end{align*}
By the induction hypothesis applied to $\mathfrak a^\perp$, there exist simple ideals
\begin{align*}
\mathfrak b_1,\dots,\mathfrak b_q \trianglelefteq \mathfrak a^\perp
\end{align*}
such that
\begin{align*}
\mathfrak a^\perp = \mathfrak b_1 \oplus \cdots \oplus \mathfrak b_q,
\qquad
[\mathfrak b_i,\mathfrak b_j]=0 \quad \text{for } i\neq j.
\end{align*}
Since each $\mathfrak a_i$ is an ideal of $\mathfrak a$ and $[\mathfrak a^\perp,\mathfrak a]=0$, each $\mathfrak a_i$ is an ideal of $\mathfrak g$. Likewise, each $\mathfrak b_j$ is an ideal of $\mathfrak g$.
[guided]
Both $\mathfrak a$ and $\mathfrak a^\perp$ are finite-dimensional semisimple Lie algebras over $F$, and both have dimension strictly smaller than $\dim_F \mathfrak g$. Therefore the induction hypothesis applies to each one.
Applied to $\mathfrak a$, the induction hypothesis gives simple ideals
\begin{align*}
\mathfrak a_1,\dots,\mathfrak a_p \trianglelefteq \mathfrak a
\end{align*}
such that
\begin{align*}
\mathfrak a = \mathfrak a_1 \oplus \cdots \oplus \mathfrak a_p,
\qquad
[\mathfrak a_i,\mathfrak a_j]=0 \quad \text{whenever } i\neq j.
\end{align*}
Applied to $\mathfrak a^\perp$, it gives simple ideals
\begin{align*}
\mathfrak b_1,\dots,\mathfrak b_q \trianglelefteq \mathfrak a^\perp
\end{align*}
such that
\begin{align*}
\mathfrak a^\perp = \mathfrak b_1 \oplus \cdots \oplus \mathfrak b_q,
\qquad
[\mathfrak b_i,\mathfrak b_j]=0 \quad \text{whenever } i\neq j.
\end{align*}
We must still check that these summands are ideals of $\mathfrak g$, not only ideals of the smaller summands. Let $u \in \mathfrak a_i$ and let $x \in \mathfrak g$. Write $x=y+z$ with $y \in \mathfrak a$ and $z \in \mathfrak a^\perp$. Since $\mathfrak a_i \trianglelefteq \mathfrak a$,
\begin{align*}
[y,u]\in \mathfrak a_i.
\end{align*}
Since $[\mathfrak a^\perp,\mathfrak a]=0$ and $u \in \mathfrak a$, we have
\begin{align*}
[z,u]=0.
\end{align*}
Therefore
\begin{align*}
[x,u]=[y+z,u]=[y,u]+[z,u]\in \mathfrak a_i.
\end{align*}
Thus $\mathfrak a_i \trianglelefteq \mathfrak g$. The same argument, with $\mathfrak a$ and $\mathfrak a^\perp$ interchanged, shows that each $\mathfrak b_j \trianglelefteq \mathfrak g$.
[/guided]
[/step]
[step:Assemble the simple ideals and verify pairwise commutation]
Set
\begin{align*}
m := p+q
\end{align*}
and list the ideals
\begin{align*}
\mathfrak g_1,\dots,\mathfrak g_m
\end{align*}
as
\begin{align*}
\mathfrak a_1,\dots,\mathfrak a_p,\mathfrak b_1,\dots,\mathfrak b_q.
\end{align*}
Using the two direct-sum decompositions and $\mathfrak g=\mathfrak a\oplus\mathfrak a^\perp$, we obtain
\begin{align*}
\mathfrak g
&=
\mathfrak a \oplus \mathfrak a^\perp \\
&=
(\mathfrak a_1 \oplus \cdots \oplus \mathfrak a_p)
\oplus
(\mathfrak b_1 \oplus \cdots \oplus \mathfrak b_q) \\
&=
\mathfrak g_1 \oplus \cdots \oplus \mathfrak g_m.
\end{align*}
The summands are simple ideals of $\mathfrak g$ by the previous step. Ideals from the same family commute by the induction hypothesis, and ideals from different families commute because
\begin{align*}
[\mathfrak a,\mathfrak a^\perp]=0.
\end{align*}
Hence $[\mathfrak g_i,\mathfrak g_j]=0$ for every $i\neq j$. This completes the induction and the proof.
[/step]