Let $A$ and $B$ be two given ordered sets with the linear (or total) order relations $<_A$ and $<_B$, respectively. Then $(A,<_A)$ and $(B,<_B)$ are said to be of the same type if there exists a bijection $f \colon A \to B$ such that $a_1 <_A a_2$ implies that $f(a_1) <_B f(a_2)$ for any pair of elements $a_1$, $a_2$ of $A$.
Furthermore, the dictionary, or lexicographical, order $<_L$ on the Cartesian product $A\times B$ is defined as follows: $a_1 \times b_1 <_L a_2 \times b_2$ if and only if the following holds:
Either $a_1 <_A a_2$, or $a_1 =a_2 $ and $b_1 <_B b_2$.
Now let's consider the two sets $Z^+ \times [0,1)$ and $ [0,1) \times Z^+$, where $Z^+$ denotes the set of positive integers and $[0,1)$ denotes the set of all non-negative reals less than $1$, both under the usual order. Let us give both these Cartesian products the dictionary, or lexicographical, order.
Then how to rigorously prove, using the above definition, that these two sets have different order types?
I know that the set $Z^+ \times [0,1)$ has the same order type as the set of non-negative real numbers under the usual order, for we can define the map $ f \colon Z^+ \times [0,1) \to [0,+\infty)$ as $$f(n\times t) \colon = n + t - 1$$ for all $n \in Z^+$ and all $t \in [0,1)$. This map is an order-preserving bijection.
I also know that every element $t \times n$ of the set $[0,1) \times Z^+$ has an immediate successor, namely the element $t \times (n+1)$.
However, this is not the case for the set $Z^+ \times [0,1)$, for if we take any two elements of this set, say, $n_1 \times t_1$ and $n_2 \times t_2$ such that $n_1 \times t_1 <_L n_2 \times t_2$, then either $n_1 < n_2$, or $n_1 = n_2$ and $t_1 < t_2$, where $n_1$ and $n_2$ are positive integers and $t_1$ and $t_2$ are real numbers in the interval $[0,1)$. If $n_1 < n_2$, then the element $n_1 \times (t_1 +1)/2$, for example, satisfies $n_1 \times t_1 <_L n_1 \times (t_1+1)/2$ and $n_1 \times (t_1 +1)/2 <_L n_2 \times t_2$. In fact, an element of the form $n_1 \times (\alpha t_1 + 1 -\alpha)$ or $n_2 \times (\alpha t_2)$ would do, where $0 < \alpha <1$. Similarly, if $n_1 = n = n_2$ and $t_1 < t_2$, then the element $n \times (\alpha t_1 + (1 - \alpha) t_2 )$, where $0 < \alpha < 1$ as before, satisfies $n_1 \times t_1 <_L n \times (\alpha t_1 + (1 - \alpha) t_2 )$ and $n \times (\alpha t_1 + (1 - \alpha) t_2 ) <_L n_2 \times t_2$. Thus we have shown that between any two distinct elements of the set $Z^+ \times [0,1)$, there is another element of $Z^+ \times [0,1)$, in fact there are infinitley many elements.