---

Step * of Lemma proj-rev_functionality

∀[n:ℕ]. ∀[p1,p2:ℙ^n].  proj-rev(n;p1) = proj-rev(n;p2) supposing p1 = p2
BY
{ (Auto THEN (All (RWO "proj-eq-iff") THENA Auto) THEN RepeatFor 4 (ParallelLast)) }

1
1. n : ℕ
2. p1 : ℙ^n
3. p2 : ℙ^n
4. m : {m:ℝ| m ≠ r0} 
5. ∀i:ℕn + 1. ((p1 i) = (m*p2 i))
6. i : ℕn + 1
7. (p1 i) = (m*p2 i)
⊢ (proj-rev(n;p1) i) = (m*proj-rev(n;p2) i)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p1,p2:\mBbbP{}\^{}n].    proj-rev(n;p1)  =  proj-rev(n;p2)  supposing  p1  =  p2


By

---

Latex:
(Auto  THEN  (All  (RWO  "proj-eq-iff")  THENA  Auto)  THEN  RepeatFor  4  (ParallelLast))

---

Home Index