---

Step * 1 1 1 of Lemma bag-combine-com


1. A : Type
2. B : Type
3. C : Type
4. f : A ⟶ B ⟶ bag(C)
5. ba : bag(A)
⊢ ⋃a∈ba.⋃b∈[].f[a;b] = ⋃b∈[].⋃a∈ba.f[a;b] ∈ bag(C)
BY
{ (Fold `empty-bag` 0 THEN (RWO "bag-combine-empty-left" 0 THENA Auto) THEN RWO "bag-combine-empty-right" 0 THEN Auto)
⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)
5.  ba  :  bag(A)
\mvdash{}  \mcup{}a\mmember{}ba.\mcup{}b\mmember{}[].f[a;b]  =  \mcup{}b\mmember{}[].\mcup{}a\mmember{}ba.f[a;b]


By

---

Latex:
(Fold  `empty-bag`  0
  THEN  (RWO  "bag-combine-empty-left"  0  THENA  Auto)
  THEN  RWO  "bag-combine-empty-right"  0
  THEN  Auto)\mcdot{}

---

Home Index