---

Step * of Lemma classfun_wf

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)].  ∀[e:E]. (X(e) ∈ T) supposing X is functional
BY
{ (Auto
   THEN D -2
   THEN (With ⌈e⌉ (D (-2))⋅ THENA Auto)
   THEN (With ⌈e⌉ (D (-3))⋅ THENA Auto)
   THEN Unfold `classrel` (-1)
   THEN Fold `single-valued-bag` (-1)
   THEN ProveWfLemma) }

1
1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. e : E
6. 1 ≤ #(X(e))
7. single-valued-bag(X es e;T)
⊢ 0 < #(X es e)

---

Latex:


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


By

(Auto
  THEN  D  -2
  THEN  (With  \mkleeneopen{}e\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto)
  THEN  (With  \mkleeneopen{}e\mkleeneclose{}  (D  (-3))\mcdot{}  THENA  Auto)
  THEN  Unfold  `classrel`  (-1)
  THEN  Fold  `single-valued-bag`  (-1)
  THEN  ProveWfLemma)

---

Home Index