---

Step * 2 of Lemma proj-permute_wf

.....set predicate..... 
1. n : ℕ
2. p : ℝ^n + 1
3. ∃k:ℕn + 1. p k ≠ r0
4. f : ℕn + 1 ⟶ ℕn + 1
5. Surj(ℕn + 1;ℕn + 1;f)
⊢ ∃k:ℕn + 1. proj-permute(p;f) k ≠ r0
BY
{ (D 3 THEN (D -1 With ⌜k⌝  THENA Auto) THEN ParallelLast THEN Auto THEN RepUR ``proj-permute`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  n  :  \mBbbN{}
2.  p  :  \mBbbR{}\^{}n  +  1
3.  \mexists{}k:\mBbbN{}n  +  1.  p  k  \mneq{}  r0
4.  f  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbN{}n  +  1
5.  Surj(\mBbbN{}n  +  1;\mBbbN{}n  +  1;f)
\mvdash{}  \mexists{}k:\mBbbN{}n  +  1.  proj-permute(p;f)  k  \mneq{}  r0


By

---

Latex:
(D  3
  THEN  (D  -1  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  RepUR  ``proj-permute``  0
  THEN  Auto)

---

Home Index