Strong definability of a numerical function
= Strong definability of a numerical function
{title2=$f(\vec n)=m\Longrightarrow S\vdash\forall y(D(\bar{\vec 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.