---

Step * of Lemma bag-filter-append

∀[p,as,bs:Top].  ([x∈as + bs|p[x]] ~ [x∈as|p[x]] + [x∈bs|p[x]])
BY
{ (Auto THEN Unfolds ``bag-filter bag-append`` 0 THEN BLemma `filter_append_sq` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p,as,bs:Top].    ([x\mmember{}as  +  bs|p[x]]  \msim{}  [x\mmember{}as|p[x]]  +  [x\mmember{}bs|p[x]])


By

---

Latex:
(Auto  THEN  Unfolds  ``bag-filter  bag-append``  0  THEN  BLemma  `filter\_append\_sq`  THEN  Auto)

---

Home Index