---

Step * of Lemma bag-combine-append-right

∀[A,B:Type]. ∀[F,G:A ⟶ bag(B)]. ∀[ba:bag(A)].  (⋃x∈ba.F[x] + G[x] = (⋃x∈ba.F[x] + ⋃x∈ba.G[x]) ∈ bag(B))
BY
{ (Auto THEN BagD (-1) THEN Auto THEN Subst ⌜⋃x∈as.F[x] + G[x] = (⋃x∈as.F[x] + ⋃x∈as.G[x]) ∈ bag(B)⌝ 0⋅ THEN Auto) }

1
.....equality..... 
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)
⊢ ⋃x∈as.F[x] + G[x] = (⋃x∈as.F[x] + ⋃x∈as.G[x]) ∈ bag(B)

2
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)
⊢ (⋃x∈as.F[x] + ⋃x∈as.G[x]) = (⋃x∈bs.F[x] + ⋃x∈bs.G[x]) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[F,G:A  {}\mrightarrow{}  bag(B)].  \mforall{}[ba:bag(A)].    (\mcup{}x\mmember{}ba.F[x]  +  G[x]  =  (\mcup{}x\mmember{}ba.F[x]  +  \mcup{}x\mmember{}ba.G[x]))


By

---

Latex:
(Auto
  THEN  BagD  (-1)
  THEN  Auto
  THEN  Subst  \mkleeneopen{}\mcup{}x\mmember{}as.F[x]  +  G[x]  =  (\mcup{}x\mmember{}as.F[x]  +  \mcup{}x\mmember{}as.G[x])\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index