---

Step * of Lemma bag-product-empty

∀[bs:Top]. ({} × bs ~ {})
BY
{ (RepUR ``bag-product empty-bag`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[bs:Top].  (\{\}  \mtimes{}  bs  \msim{}  \{\})


By

---

Latex:
(RepUR  ``bag-product  empty-bag``  0  THEN  Auto)

---

Home Index