---

Step * 2 1 of Lemma bag-combine-append-right


1. A : Type
2. B : Type
3. F : A ⟶ bag(B)
4. G : A ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. as = bs ∈ bag(A)
9. as ∈ bag(A)
10. bs ∈ bag(A)
⊢ (⋃x∈as.F[x] + ⋃x∈as.G[x]) = (⋃x∈bs.F[x] + ⋃x∈bs.G[x]) ∈ bag(B)
BY
{ RepeatFor 2 ((EqCD THEN Auto)) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  F  :  A  {}\mrightarrow{}  bag(B)
4.  G  :  A  {}\mrightarrow{}  bag(B)
5.  as  :  A  List
6.  bs  :  A  List
7.  permutation(A;as;bs)
8.  as  =  bs
9.  as  \mmember{}  bag(A)
10.  bs  \mmember{}  bag(A)
\mvdash{}  (\mcup{}x\mmember{}as.F[x]  +  \mcup{}x\mmember{}as.G[x])  =  (\mcup{}x\mmember{}bs.F[x]  +  \mcup{}x\mmember{}bs.G[x])


By

---

Latex:
RepeatFor  2  ((EqCD  THEN  Auto))

---

Home Index