---

Step * 1 1 of Lemma equipollent-product-one


ℕ1 ~ Unit
BY
{ TACTIC:(BLemma `equipollent-unit` THEN Auto) }

1
ℕ1

---

Latex:

---

Latex:

\mBbbN{}1  \msim{}  Unit


By

---

Latex:
TACTIC:(BLemma  `equipollent-unit`  THEN  Auto)

---

Home Index