Theorem: Derivative of Product of Operator-Valued Functions

Let $\struct {X, \norm \cdot_X}$, $\struct {Y, \norm \cdot_Y}$, and $\struct {Z, \norm \cdot_Z}$ normed vector spaces.
Let $\map B {X, Y}$, $\map B {Y, Z}$ and $\map B {X, Z} $ denote the space of bounded linear transformations between $X$ and $Y$, between $Y$ and $Z$, and between $X$ and $Z$, respectively.
Let $A : I \to \map B {X, Y}$ and $B : I \to \map B {Y, Z}$ be differentiable mappings defined on an interval $I$ whose images are bounded linear transformations.
The product $A B: I \to \map B {X, Z}: x \mapsto \map A x \map B x$ is differentiable and its derivative at any $x \in \R$ is given by $\map {A'} x \map B x + \map A x \map {B'} x$.

Proof:
Given arbitrary $x, h \in I$ such that $h \ne 0$, $x+h\in I$ we compute:
:$\norm {\dfrac {\map {\paren {A B} } {x + h} - \map {\paren {A B} } x} h - \map {A'} x \map B x - \map A x \map {B'} x}_{\map B {X, Z} }$
to be:
{{begin-eqn}}
{{eqn | o = 
      | r = \norm {\dfrac {\map A {x + h}\map B {x + h} - \map A x \map B x} h-\map {A'} x \map B x - \map A x \map {B'} x}_{\map B {X, Z} }
      | c = Definition of $AB$
}}
{{eqn | r = \norm {\dfrac {\map A {x + h}\map B {x + h} - \map A x \map B {x + h} + \map A x \map B {x + h} - \map A x \map B x} h-\map {A'} x \map B {x + h} + \map {A'} x \map B {x + h} - \map {A'} x \map B x - \map A x \map {B'} x}_{\map B {X, Z} }
      | c = expanding
}}
{{eqn | o = \le
      | r = \norm {\dfrac {\map A {x + h} \map B {x + h} - \map A x \map B {x + h} } h-\map {A'} x \map B {x + h} }_{\map B {X, Z} } + \norm {\map {A'} x \map B {x + h} - \map {A'} x \map B x }_{\map B {X, Z} } + \norm {\dfrac {\map A x \map B {x + h} - \map A x \map B x} h - \map A x \map {B'} x}_{\map B {X, Z} }
      | c = {{NormAxiomVector|3}}
}}
{{eqn | r = \norm {\paren {\dfrac {\map A {x + h} - \map A x } h - \map {A'} x} \map B {x + h} }_{\map B {X, Z} } + \norm {\map {A'} x \paren {\map B {x + h} - \map B x} }_{\map B {X, Z} } + \norm {\map A x \paren {\dfrac {\map B {x + h} - \map B x} h - \map {B'} x} }_{\map B {X, Z} }
      | c = factoring
}}
{{eqn | o = \le
      | r = \norm {\dfrac {\map A {x + h} - \map A x} h - \map {A'} x}_{\map B {X, Y} } \norm {\map B {x + h} }_{\map B {Y, Z} } + \norm {\map {A'} x}_{\map B {X, Y} } \norm {\map B {x + h} - \map B x}_{\map B {Y, Z} } + \norm {\map A x}_{\map B {X, Y} } \norm {\dfrac {\map B {x + h} - \map B x} h - \map {B'} x}_{\map B {Y, Z} }
      | c = Norm on Bounded Linear Transformation is Submultiplicative
}}
{{end-eqn}}
$\norm {\dfrac {\map A {x + h} - \map A x} h - \map {A'} x}_{\map B {X, Y} }$ vanishes as $h \to 0$ because $\map {A'} x$ is the derivative of $A$ at $x$ which exists by assumption.
$\norm {\dfrac {\map B {x + h} - \map B x} h - \map {B'} x}_{\map B {Y, Z} }$ vanishes as $h \to 0$ because $\map {B'} x$ is the derivative of $B$ at $x$ which exists by assumption.
$\norm {\map B {x + h} - \map B x  }_{\map B {Y, Z} }$ vanishes as $h \to 0$ by Differentiable Operator-Valued Function is Continuous.
By the Reverse Triangle Inequality:
:$\size {\norm {\map B {x + h} }_{\map B {Y, Z} } - \norm {\map B x}_{\map B {Y, Z} } } \le \norm {\map B {x + h} - \map B x}_{\map B {Y, Z} } \to 0$
as $h \to 0$.
Together this shows:
:$\ds \lim_{h \mathop \to 0} \norm {\frac {\map {\paren {A B} } {x + h} - \map {\paren {A B} } x} h - \map {A'} x \map B x - \map A x \map {B'} x}_{\map B {X, Z} } = 0$
Therefore the derivative of $A B$ at $x$ is:
:$\map {A'} x \map B x + \map A x \map {B'} x$
{{qed}}