---

Step * of Lemma classfun-eclass3

∀[Info,B,C:Type]. ∀[X:EClass(B ⟶ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  (eclass3(X;Y)(e) = (X(e) Y(e)) ∈ C) supposing (X is functional and Y is functional)
BY
{ (Auto
   THEN Fold `classfun-res` 0
   THEN RWO "classfun-res-eclass3" 0
   THEN Auto
   THEN RepeatFor 2 ((Using [`e',⌜e⌝] (FLemma `es-functional-class-implies-at` [-2])⋅ THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  C)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (eclass3(X;Y)(e)  =  (X(e)  Y(e)))  supposing  (X  is  functional  and  Y  is  functional)


By

---

Latex:
(Auto
  THEN  Fold  `classfun-res`  0
  THEN  RWO  "classfun-res-eclass3"  0
  THEN  Auto
  THEN  RepeatFor  2  ((Using  [`e',\mkleeneopen{}e\mkleeneclose{}]  (FLemma  `es-functional-class-implies-at`  [-2])\mcdot{}  THENA  Auto))
  THEN  Auto)

---

Home Index