---

Step * of Lemma class-output-eq

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[bg:bag(E)].
  (class-output(X;es;bg) = ∪e∈class-output-support(es;bg).X es e ∈ bag(T))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``class-output class-output-support class-le-before`` 0
   THEN RWO "bag-combine-assoc" 0⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[bg:bag(E)].
    (class-output(X;es;bg)  =  \mcup{}e\mmember{}class-output-support(es;bg).X  es  e)


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``class-output  class-output-support  class-le-before``  0
  THEN  RWO  "bag-combine-assoc"  0\mcdot{}
  THEN  Auto)

---

Home Index