Can we be certain that the only nonzero differentiable function satisfying $g(x+y)=\frac{g(x)+g(y)}{1+g(x)g(y)}$ and $|g|\lt 1$ is $\tanh(kx)$? The following question is a question aimed for the Further Maths UK syllabus (it is a Step $2$ question)- i.e. not very formal, so I am certain my solution to the question is correct as the question intended it, but I am uncertain whether it is formally the only, or the right, solution. I am especially uncertain about my application of the Picard existence & uniqueness theorem.
The problem:

The function $g$ has derivative $g'$ and satisfies: $$g(x+y)=\frac{g(x)+g(y)}{1+g(x)g(y)}$$For all $x$ and $y$, $|g(x)|\lt 1$ for all $x$, and $g'(0)=k\neq0$. Find $g'(x)$ in terms of $g(x)$ and $k$, and hence find $g(x)$ in terms of $x$ and $k$.

My solution (but is it unique, and is it rigorously done?):

Consider the difference quotient for $y\neq 0$, some $x\in\Bbb R$: $$\tag{1}\frac{g(x+y)-g(x)}{y}=(1-g^2(x))\cdot\frac{g(y)}{y(1+g(x)g(y))}$$First note that $|g(x)|\lt1$ gives $(1-g^2(x))\neq0$ and $1+g(x)g(y)\neq0$. Secondly, if $g'(0)\neq0$ we must have that the numerator of the difference quotient must be nonzero in some small deleted neighbourhood of $0$ (else we could take a convergent sequence $y_n\to0$ where $g(y_n)=0$ for all $n$, and then $g'(0)=0$ if the limit exists) so if we set $x=0$, we may divide by $g(y)$ in the above with $y$ close to $0$ but $g(y)\neq0$: $$\frac{g(y)-g(0)}{y}=(1-g^2(0))\cdot\frac{1}{\frac{y}{g(y)}+y\cdot g(0)}$$For the above limit as $y\to0$ to exist, the limit as $y\to0$ of the denominator must exist: as $\lim_{y\to0}y\cdot g(0)$ exists (and equals $0$) we conclude $\lim_{y\to0}\frac{y}{g(y)}$ must exist, giving: $$\begin{align}k=\lim_{y\to0}\frac{g(y)-g(0)}{y}&=(1-g^2(0))\cdot\frac{1}{\lim_{y\to0}\frac{y}{g(y)}}\\\lim_{y\to0}\frac{g(y)}{y}&=\frac{k}{(1-g^2(0))}\end{align}$$This further implies that $g(y)\to0$ as $y\to0$ and by continuity of differentiable functions $g(0)=0$, so that: $$k=\lim_{y\to0}\frac{g(y)}{y}=\lim_{y\to0}\frac{g(y)-g(0)}{y}$$Using the same argument that $g(y)\neq 0$ in some small deleted neighbourhood of $0$ and dividing by $g(y)$ in $(1)$, for now arbitrary $x$, we get: $$g'(x)=\lim_{y\to0}\frac{g(x+y)-g(x)}{y}=(1-g^2(x))\cdot\lim_{y\to0}\frac{g(y)}{y}=(1-g^2(x))\cdot k$$

The differential equation $g'(x)=k(1-g^2(x))$ has a solution in $g(x)=\tanh(kx)$. I think that by the Picard existence theorem, the solution is unique since $|g(x)|\lt 1$ gives a Lipschitz bound on $k(1-g^2(x))$, although even then we only have uniqueness potentially in some small interval around $0$. Can we really conclude $g(x)=\tanh(kx)$ with certainty? And just how necessary is the condition $|g(x)|\lt1$?
 A: Here's what we can show:

If $f:\Bbb{R}\to\Bbb{R}$ is a differentiable function such that $f'(0)=1$, and such that for all $x,y\in\Bbb{R}$, $f(x+y)[1+f(x)f(y)]=f(x)+f(y)$, then $f=\tanh$.

For the proof we first plug in $y=0$ to get that for all $x\in\Bbb{R}$, we have $f(x)^2f(0)=f(0)$. If $f(0)\neq 0$, we have $f(x)^2=1$ for all $x$, and hence by continuity $f=1$ or $f=-1$, contradicting that $f'(0)=1$. Therefore, $f(0)=0$. Next, we have for all $x,y\in\Bbb{R}$ that
\begin{align}
f(x+y)-f(x)&= f(x+y)-\bigg(f(x+y)[1+f(x)f(y)]-f(y)\bigg)\\
&=-f(x+y)f(x)f(y)+f(y)\\
&=f(y)[1-f(x+y)f(x)]
\end{align}
Assuming $y\neq 0$, we can now divide by $y$ and take the limit $y\to 0$, and use the fact that $f(0)=0$ and $f'(0)=1$ to deduce $f'(x)=1-f(x)^2$. So, $f$ is a differentiable function satisfying the ODE $f'=1-f^2$ (so by induction it is actually $C^{\infty}$) and $f(0)=0$. In the language of ODEs, if we define $\Phi:\Bbb{R}\to\Bbb{R}$ as $\Phi(\xi)=1-\xi^2$, then $\Phi$ is locally Lipschitz, and $f$ satisfies $f'=\Phi\circ f$ with $f(0)=0$, i.e it is a solution of the IVP
\begin{align}
\begin{cases}
\xi'=\Phi(\xi)\\
\xi(0)=0
\end{cases}
\end{align}
For such (locally Lipschitz) ODEs, we have local existence and uniqueness. However, we already know a global solution exists, namely $\tanh$. Therefore, by uniqueness, $f=\tanh$.

Now, regarding $g$ and the assumption $g'(0)=k\neq 0$, this is easily reduced to the case $k=1$ by considering $x\mapsto g(\frac{x}{k})$.
So, your answer is essentially right, though it can be streamlined as shown above. The assumption $|g|<1$ is superfluous as shown above. More importantly, the assumption $|g|<1$ is not what's required to invoke the uniqueness results from ODEs. That theorem requires that $\Phi$ (i.e the RHS) satisfy certain regularity conditions, not that the solution you're looking for (i.e $g$) satisfy certain bounds.
A: We know that $\tanh(x)=\frac{e^{2x}-1}{e^{2x}+1}$. Thus set $g=\frac{f-1}{f+1}$, so that $f=\frac{1+g}{1-g}$. This is non-singular everywhere due to the assumption $|g|<1$.
Then
\begin{align}
f(x+y)=\frac{1+g(x)g(y)+g(x)+g(y)}{1+g(x)g(y)-g(x)-g(y)}=f(x)f(y)
\end{align}
So $f(x)=e^{cx}$ follows for $g$ differentiable. Set $c=2k$.
