---

Step * 1 of Lemma d-conv_wf

.....assertion..... 
∀n:ℕ. (two-factorizations(n) ∈ bag(ℕ × ℕ))
BY
{ xxx(D 0 THENA Auto)xxx }

1
1. n : ℕ
⊢ two-factorizations(n) ∈ bag(ℕ × ℕ)

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}n:\mBbbN{}.  (two-factorizations(n)  \mmember{}  bag(\mBbbN{}  \mtimes{}  \mBbbN{}))


By

---

Latex:
xxx(D  0  THENA  Auto)xxx

---

Home Index