Let $R$ be a (commutative or non-commutative) unital ring, $X$ be a non-empty set, and $R \langle\! \langle X \rangle\! \rangle$ be the ordered series ring (in fact, a ring of formal power series over $R$ in $|X|$ non-commuting variables) obtained by endowing the set of all functions $\mathscr F(X) \to R$ with the usual operations of pointwise addition and Cauchy product. Here, $\mathscr F(X)$ is the free monoid on $X$, whose operation (that is, word concatenation) I'll denote by $\ast$.

While looking for a counterexample to a certain property in the class of local rings, I happened to note that, for each $z \in X$, the mapping $\partial_z$ that sends an ordered series $f \in R \langle\! \langle X \rangle\! \rangle$ to the function $$ \mathscr F(X) \to R \colon \mathfrak z \mapsto \sum_{(\mathfrak u, \mathfrak v) \in \mathscr F(X) \times \mathscr F(X): \mathfrak u \ast z \ast \mathfrak v = \mathfrak z} f(\mathfrak u \ast \mathfrak v), $$ is a well-defined derivation of $R \langle\! \langle X \rangle\! \rangle$. In particular, the Leibniz identity follows from the fact that $\mathscr F(X)$ is a cancellative monoid with trivial group of units and every $X$-word factors uniquely in $\mathscr F(X)$ as a product of elements of $X$ (that is, $X$-words of length one).

My question is whether anyone here can offer a reference where $\partial_z$ is being introduced: I thought I would have found $\partial_z$ defined in Cohn's book on FIRs (where ordered series rings are discussed in Sect. 1.5), but it's not there (as far as I can see). I've also tried with Lam's A First Course in Noncommutative Rings, but the conclusion is the same.