The Operator-Norm Distance between Real Matrices Is a Map

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $m,n\in\mathbb{N}$, with the real matrices $\mathcal{M}_{m\times n}(\mathbb{R})$, their difference $A-B$, and the operator norm $\lVert\cdot\rVert$, a map $\mathcal{M}_{m\times n}(\mathbb{R})\to\mathbb{R}$ by The Operator Norm of a Real Matrix §norm.

¶ There is exactly one map $d:\mathcal{M}_{m\times n}(\mathbb{R})\times\mathcal{M}_{m\times n}(\mathbb{R})\to\mathbb{R}$ with $d(A,B)=\lVert A-B\rVert$ for all $A,B\in\mathcal{M}_{m\times n}(\mathbb{R})$.