---

Step * 1 of Lemma prime-factors-unique

.....assertion..... 
∀ps,qs:{m:ℕ| prime(m)}  List.  ((Π(ps)  = Π(qs)  ∈ ℤ) ⇒ permutation(ℤ;ps;qs))
BY
{ Unfold `mul-list` 0 }

1
∀ps,qs:{m:ℕ| prime(m)}  List.  ((reduce(λx,y. (x * y);1;ps) = reduce(λx,y. (x * y);1;qs) ∈ ℤ) ⇒ permutation(ℤ;ps;qs))

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}ps,qs:\{m:\mBbbN{}|  prime(m)\}    List.    ((\mPi{}(ps)    =  \mPi{}(qs)  )  {}\mRightarrow{}  permutation(\mBbbZ{};ps;qs))


By

---

Latex:
Unfold  `mul-list`  0

---

Home Index