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$?
Here's what we can show:
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.