---

Step * of Lemma classfun-res-eclass1

∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ C]. ∀[es:EO+(Info)]. ∀[e:E].
  ((f o X)@e = (f loc(e) X@e) ∈ C) supposing (single-valued-classrel(es;X;B) and (↑e ∈b X))
BY
{ (Auto
   THEN RepUR ``eclass1 classfun-res classfun class-ap`` 0
   THEN BLemma `sv-bag-only-map2`
   THEN Auto
   THEN Try (Complete (ProveSingleVal))
   THEN BLemma `member-eclass-iff-size`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    ((f  o  X)@e  =  (f  loc(e)  X@e))  supposing  (single-valued-classrel(es;X;B)  and  (\muparrow{}e  \mmember{}\msubb{}  X))


By

---

Latex:
(Auto
  THEN  RepUR  ``eclass1  classfun-res  classfun  class-ap``  0
  THEN  BLemma  `sv-bag-only-map2`
  THEN  Auto
  THEN  Try  (Complete  (ProveSingleVal))
  THEN  BLemma  `member-eclass-iff-size`
  THEN  Auto)

---

Home Index