---

Step * of Lemma eclass3-functional

∀[Info,B,C:Type]. ∀[X:EClass(B ⟶ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)].
  (eclass3(X;Y) is functional) supposing (X is functional and Y is functional)
BY
{ (Auto
   THEN All(Unfold `es-functional-class`)
   THEN D 0
   THEN Try ((BLemma `eclass3-single-val` THEN Auto))
   THEN Try ((BLemma `eclass3-total` THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  All(Unfold  `es-functional-class`)
  THEN  D  0
  THEN  Try  ((BLemma  `eclass3-single-val`  THEN  Auto))
  THEN  Try  ((BLemma  `eclass3-total`  THEN  Auto)))

---

Home Index