---

Step * of Lemma bag_all-map

∀[b,f,g:Top].  (bag_all(bag-map(g;b);f) ~ bag_all(b;f o g))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``bag_all`` 0
   THEN (RWO "bag-accum-map" 0 THENA Auto)
   THEN RepUR ``compose so_apply`` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``bag\_all``  0
  THEN  (RWO  "bag-accum-map"  0  THENA  Auto)
  THEN  RepUR  ``compose  so\_apply``  0
  THEN  Auto)

---

Home Index