---

Step * of Lemma bag-combine-size

∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[ba:bag(A)].  (#(⋃a∈ba.f[a]) = bag-sum(ba;a.#(f[a])) ∈ ℕ)
BY
{ (Auto THEN BagD (-1) THEN Auto THEN Subst' bag-sum(bs;a.#(f[a])) = #(⋃a∈bs.f[a]) ∈ ℕ 0) }

1
.....equality..... 
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
⊢ bag-sum(bs;a.#(f[a])) = #(⋃a∈bs.f[a]) ∈ ℕ

2
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
⊢ #(⋃a∈as.f[a]) = #(⋃a∈bs.f[a]) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[ba:bag(A)].    (\#(\mcup{}a\mmember{}ba.f[a])  =  bag-sum(ba;a.\#(f[a])))


By

---

Latex:
(Auto  THEN  BagD  (-1)  THEN  Auto  THEN  Subst'  bag-sum(bs;a.\#(f[a]))  =  \#(\mcup{}a\mmember{}bs.f[a])  0)

---

Home Index