Strong definability of a numerical function ($f(\vec{n})=m⟹S⊢\forall y(D(\overline{\stackrel{⃗}{n}},y)\leftrightarrow y=\bar{m})$)

Strong definability of a numerical function adds internal uniqueness of the output at every standard input tuple. Together with a proved correct instance, this says the first-order theory proves that the output logical formula is equivalent to logical equality with the correct numeral, for arbitrary potential outputs.