---

Step * of Lemma int-bag-product-append

∀[b1,b2:bag(ℤ)].  (Π(b1 + b2) ~ Π(b1) * Π(b2))
BY
{ (Auto
   THEN RepUR ``int-bag-product bag-product`` 0
   THEN (RWO "bag-summation-append" 0 THEN Auto)
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[b1,b2:bag(\mBbbZ{})].    (\mPi{}(b1  +  b2)  \msim{}  \mPi{}(b1)  *  \mPi{}(b2))


By

---

Latex:
(Auto
  THEN  RepUR  ``int-bag-product  bag-product``  0
  THEN  (RWO  "bag-summation-append"  0  THEN  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index