Let $X$ be a compact metric space. Recall that the ultralimit along an
ultrafilter $\U$ of a set of subsets $Y_i (= X$ is $\lim_{i --> \U} Y_i = \{
\lim_{i --> \U} y_i | y_i (- Y_i \}$; equivalently, $x (- \lim_{i --> \U} Y_i$
iff for every neighbourhood $U -) x$, $\{ i | U \cap Y_i /= {} \} (- \U$.

Now suppose each $Y_i$ 

So from the point of view of metric logic, $\S'$
viewed as a direct limit of its bounded subsets is rather uninteresting, being
analogous to a directed system of finite structures. Nonetheless, we consider
it this way, giving us a notion of ultraproduct and a corresponding Łos
theorem. In fact we will apply this only to structures which can be embedded
as subspaces of $\S'$, for which the ultraproduct becomes the topological
ultralimit within $\S'$:

Lemma:
      Let $X$ be a compact metric space, and let $Y_i$ be subspaces. Consider
      $X$ and $Y_i$ as metric structures with no structure other than the
      metric.

      Then the map $\Pi_{i -> \U} y_i |-> \lim_{i -> \U} y_i$, the latter limit
      being well-defined since $X$ is compact Hausdorff, yields an isomorphism
      between the continuous ultraproduct $\Pi_{i -> \U} Y_i$ and the
      topological ultralimit $\lim_{i -> \U} Y_i$ within $X$.

      Moreover, if the $Y_i$ are equipped with continuous relations
      $R^{Y_i} : Y_i^n --> \R$ with a common uniform continuity modulus, then
      $R$ is interpreted in the ultraproduct as $R^X(\lim_{i -> \U} y_i) =
      \lim_{i -> \U} R^{Y_i}(y_i)$.

      Similarly, if the $Y_i$ are equipped with continuous functions
      $f^{Y_i} : Y_i^n --> Y_i^m$ with a common uniform continuity modulus, then
      $f^X(\lim_{i -> \U} y_i) = \lim_{i -> \U} f^{Y_i}(y_i)$.

      In particular, any ultrapower of $X$ is isomorphic to $X$.

Proof:
    Immediate from definitions.

---

We apply this to functions by considering their graphs. If $f$ is interpreted
on $Y_i$ as a partial function $Y_i^n --> Y_i^m$, say it is _provably bounded_
if for every $B (- \B$ there exists $B' (- \B$ such that $f^{Y_i}(B) (= B'$
holds $\U$-often. Then $\lim_{i-->\U} f^{Y_i} y_i$ exists when $y_i (-
\dom(f^{Y_i})$. So define $f^X(\lim_{i --> \U}) := \lim_{i-->\U} f^{Y_i} y_i$
if this is well-defined for $y_i (- \dom(f^{Y_i})$.

---