---

Step * of Lemma bag-map-mapfilter

∀[b,P,f,g:Top].  (bag-map(g;bag-mapfilter(f;P;b)) ~ bag-mapfilter(g o f;P;b))
BY
{ (Auto THEN RepUR ``bag-mapfilter`` 0 THEN RWO "bag-map-map" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[b,P,f,g:Top].    (bag-map(g;bag-mapfilter(f;P;b))  \msim{}  bag-mapfilter(g  o  f;P;b))


By

---

Latex:
(Auto  THEN  RepUR  ``bag-mapfilter``  0  THEN  RWO  "bag-map-map"  0  THEN  Auto)

---

Home Index