---

Step * of Lemma eclass0-single-val

∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ bag(C)]. ∀[es:EO+(Info)].
  (single-valued-classrel(es;(f o X);C)) supposing 
     (single-valued-classrel(es;X;B) and 
     (∀i:Id. ∀b:B.  single-valued-bag(f i b;C)))
BY
{ (UnivCD THENA Auto) }

1
1. Info : Type
2. B : Type
3. C : Type
4. X : EClass(B)
5. f : Id ─→ B ─→ bag(C)
6. es : EO+(Info)
7. ∀i:Id. ∀b:B.  single-valued-bag(f i b;C)
8. single-valued-classrel(es;X;B)
⊢ single-valued-classrel(es;(f o X);C)

---

Latex:


\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].  \mforall{}[es:EO+(Info)].
    (single-valued-classrel(es;(f  o  X);C))  supposing 
          (single-valued-classrel(es;X;B)  and 
          (\mforall{}i:Id.  \mforall{}b:B.    single-valued-bag(f  i  b;C)))


By

(UnivCD  THENA  Auto)

---

Home Index