# HG changeset patch
# User Benedikt Fluhr <http://bfluhr.com>
# Date 1497839097 -7200
#      Mon Jun 19 04:24:57 2017 +0200
# Node ID f703c96ee5ea60295b051becc7e5b5cd14eb7ef5
# Parent  351059c72074d939649d10f568f83101e3806f79
Proof of Compatibility Lemma

diff --git a/00_12_EqualityOfInterlDist.md b/00_12_EqualityOfInterlDist.md
--- a/00_12_EqualityOfInterlDist.md
+++ b/00_12_EqualityOfInterlDist.md
@@ -29,6 +29,7 @@
 
 (@CpiEIso) **Lemma.**
 The homomorphism $(\mathcal{C} \circ \pi \circ \mathcal{E})_f$
+from $\mathcal{C} \mathcal{E} f$ to $\mathcal{C} \mathcal{R} \mathcal{E} f$
 is an isomorphism of precosheaves.
 
 Now $\mathbf{C}$ is closed under isomorphisms and thus also
@@ -37,7 +38,7 @@
 We note that for any continuous function
 $g \colon Y \rightarrow (-\infty, \infty]$ and
 $r \in (-\infty, \infty]$ we have
-$r + g = \mathcal{S}((-r, -r)) (g)$
+$r + g = \mathcal{S}((\infty, -r)) (g)$
 by definition of $\mathcal{S}$.
 We now recall that we also defined the endofunctors
 associated to the smoothing functor
@@ -71,6 +72,38 @@
  (\pi^2_* \circ \mathcal{C} \circ \mathcal{S}(\mathbf{a} \preceq \mathbf{b})
   \circ \mathcal{E})_f$.
 
+* *Proof.*
+First we set $(a', a) := \mathbf{a}$ and $(b', b) := \mathbf{b}$.
+Now let $r \in \R$.
+If we unravel the definitions we obtain
+$(\overline{\mathcal{S}}(\mathbf{a}) \pi^2_* \mathcal{C} \mathcal{E} f)(
+  [-\infty, r)
+ ) =
+ \Lambda(\epi f \cap X \times [-\infty, r + a))$
+and
+$(\overline{\mathcal{S}}(\mathbf{b}) \pi^2_* \mathcal{C} \mathcal{E} f)(
+  [-\infty, r)
+ ) =
+ \Lambda(\epi f \cap X \times [-\infty, r + b))$.
+Let $i$ be the inclusion of $\epi f \cap X \times [-\infty, r + a)$
+into $\epi f \cap X \times [-\infty, r + b)$
+and let
+$\tau \colon \epi f \cap X \times [-\infty, r + a) \rightarrow
+ \epi f \cap X \times [-\infty, r + b),
+ (p, t) \mapsto (p, t - a + b)$,
+then
+$(\overline{\mathcal{S}}(\mathbf{a} \preceq \mathbf{b}) \circ
+  \pi^2_* \circ \mathcal{C} \circ \mathcal{E})_{f [-\infty, r)} = \Lambda(i)$
+and
+$(\pi^2_* \circ \mathcal{C} \circ \mathcal{S}(\mathbf{a} \preceq \mathbf{b})
+  \circ \mathcal{E})_{f [-\infty, r)} = \Lambda(\tau)$.
+Now let $(p, t) \in \epi f \cap X \times [-\infty, r + a)$,
+then $\{p\} \times [t, t - a + b]$ is contained in
+$\epi f \cap X \times [-\infty, r + b)$.
+Moreover we have
+$(p, t), (p, t - a + b) \in \{p\} \times [t, t - a + b]$,
+hence $\Lambda(i) = \Lambda(\tau)$.
+
 * **Corollary.**
 We have
 $(\mathcal{S}'(\mathbf{a} \preceq \mathbf{b}) \circ