---

Step * of Lemma es-functional-class-implies-at

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)].  ∀[e:E]. X is functional at e supposing X is functional
BY
{ (Auto
   THEN D (-2)
   THEN (D 0 THEN Auto)
   THEN RWO "assert-member-eclass" 0
   THEN Auto
   THEN Unfold `es-total-class` (-2)
   THEN (InstHyp [⌈e⌉] (-2)⋅ THENA Auto)
   THEN Unfold `classrel` 0
   THEN Fold `class-ap` 0
   THEN BLemma `bag-member-iff-size`
   THEN Auto) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].
    \mforall{}[e:E].  X  is  functional  at  e  supposing  X  is  functional


By

(Auto
  THEN  D  (-2)
  THEN  (D  0  THEN  Auto)
  THEN  RWO  "assert-member-eclass"  0
  THEN  Auto
  THEN  Unfold  `es-total-class`  (-2)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Unfold  `classrel`  0
  THEN  Fold  `class-ap`  0
  THEN  BLemma  `bag-member-iff-size`
  THEN  Auto)

---

Home Index