---

Step * of Lemma equipollent-product-zero

∀[A:Type]. (A × ℕ0 ~ ℕ0 ∧ ℕ0 × A ~ ℕ0)
BY
{ Auto }

1
1. [A] : Type
⊢ A × ℕ0 ~ ℕ0

2
1. [A] : Type
2. A × ℕ0 ~ ℕ0
⊢ ℕ0 × A ~ ℕ0

---

Latex:

---

Latex:
\mforall{}[A:Type].  (A  \mtimes{}  \mBbbN{}0  \msim{}  \mBbbN{}0  \mwedge{}  \mBbbN{}0  \mtimes{}  A  \msim{}  \mBbbN{}0)


By

---

Latex:
Auto

---

Home Index