From Barry Mazur's Imagining Numbers: (particularly the square root of minus fifteen), p. 97:
Suppose that you have some unknown operation that allows, as its "input," any two positive whole numbers $M$ and $N$ and produces, as a result, another whole number, which we will denote $M*N$. [...] Suppose further that we know our mystery operation satisfies the two simple laws $(a)$ and $(b)$:
(a) For any positive whole number $N$, $$ 1*N=N $$
(b) For any three positive whole numbers $A$, $B$, and $C$, $$ A*C+B*C=(A+B)*C; $$ that is, the distributive law holds.
Then we can show that our mystery operation $*$ is none other than multiplication.
[...] A formal treatment of our subject would offer, at this point, a proof that these laws - (a) and (b) - do indeed characterize the operation of multiplication, as defined, say, by the creeping strategy.
Question: Formally and precisely, what's the result we would prove ?
What Mazur is saying is that any function $\mu: \mathbb N \to \mathbb N$ satisfying $\mu(1,n)=n$ and $\mu(a,c)+\mu(b,c)=\mu(a+b,c)$ must be ordinary multiplication given by $\mu(a,b)=a\cdot b$.
This follows by induction: $$ \mu(1+b,c)=c+\mu(b,c)=\mu(1,c)+b\cdot c=c+b\cdot c=(c+1)\cdot b $$ with the base case $$ \mu(1,n)=n=1\cdot n $$
This is usually the definition of multiplication from the Peano axioms.