Is $\left( {{\partial ^2 f}\over{\partial t\,\partial s}}\right)\bigg|_{t = s = 0} = ab - ba?$ This is a followup to my previous question here.
Let $a, b \in M_n(\mathbb{R})$. Consider the function$$f: \mathbb{R}^2 \to M_n(\mathbb{R}), \text{ }(t, s) \mapsto e^{t \cdot a} e^{s \cdot b} e^{-t \cdot a} e^{-s \cdot b}.$$In my previous question, I asked for a way to see that such function is infinitely differentiable.
Can anyone supply a rigorous proof of the fact that$$\left( {{\partial ^2 f}\over{\partial t\,\partial s}}\right)\bigg|_{t = s = 0} = ab - ba?$$All proofs I've tried coming up with I feel lack rigour...

First, note that we do have the usual product rule $(fg)' = f'g + fg'$
 for taking (partial) derivatives when products don't commute. I won't go through the details here, but the exact same proof that works for functions $\mathbb{R} \to \mathbb{R}$ goes through. Extending to multi-term products, we get:
\begin{align*}
  (fghr)' &= f'(ghr) + f(ghr)' \\
  &= f'ghr + fg'hr + fg(hr)' \\
  &= f'ghr + fg'hr + fgh'r + fghr'.
\end{align*}
Furthermore, the rule $(e^{ta})' = ae^{ta}$ applies: the usual proof using a series expansion works. You can show either of these facts yourself, using proofs found in any advanced calculus book as a template if you can't remember how they go.
Put our rules (explicitly mentioned above) together to find
\begin{align*}
  \frac{\partial f}{\partial s}
  &= e^{ta}be^{sb}e^{-ta}e^{-sb} \\
  &- e^{ta}e^{sb}e^{-ta}be^{-sb}.
\end{align*}
Differentiating again (and being careful about signs), we get:
\begin{align*}
  \frac{\partial^2 f}{\partial t \partial s}
  &= ae^{ta}be^{sb}e^{-ta}e^{-sb} \\
  &- e^{ta}be^{sb}ae^{-ta}e^{-sb} \\
  &- ae^{ta}e^{sb}e^{-ta}be^{-sb} \\
  &+ e^{ta}e^{sb}ae^{-ta}be^{-sb}.
\end{align*}
When we substitute $s,t = 0$, all the exponentials become 1, so we get
$$ ab - ba - ab + ab, $$
which simplifies to
$$ ab - ba $$
as desired.
