---

Step * of Lemma es-filter-image-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(Top)]. ∀[e:E].  f[X](e) ~ only(f X(e)) supposing ↑e ∈b X
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN RepUR ``es-filter-image eclass in-eclass 
           eclass-compose1 eclass-val`` 0⋅
   THEN AutoSplit) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Top].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    f[X](e)  \msim{}  only(f  X(e))  supposing  \muparrow{}e  \mmember{}\msubb{}  X


By

(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  RepUR  ``es-filter-image  eclass  in-eclass 
                  eclass-compose1  eclass-val``  0\mcdot{}
  THEN  AutoSplit)

---

Home Index