Homomorphisms and Isomorphisms of Ordered Fields

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $r$, with $+$, $\cdot$, $0_{r}$, $1_{r}$ and $\le$, and $s$, with $+$, $\cdot$, $0_{s}$, $1_{s}$ and $\le$, be ordered fields, and let $f:r\to s$ be a map. The operations and orders of $r$ and $s$ are written alike, as The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §overloading allows; below, those applied to $x$ and $y$ are the ones of $r$, and those applied to values of $f$ are the ones of $s$, even if $r$ and $s$ have the same elements.

¶ $f$ is a homomorphism of ordered fields if $f(1_{r})=1_{s}$ and, for all $x,y\in r$, $f(x+y)=f(x)+f(y)$, $f(x\cdot y)=f(x)\cdot f(y)$, and $x\le y$ implies $f(x)\le f(y)$.

¶ $f$ is an isomorphism of ordered fields if it is a bijective homomorphism of ordered fields and, for all $x,y\in r$, $f(x)\le f(y)$ implies $x\le y$.