---

Step * 2 of Lemma req-vec-extend


1. k : ℕ+
2. a : ℝ^k - 1
3. b : ℝ^k - 1
4. z : ℝ
5. u : ℝ
6. req-vec(k;a++z;b++u)
⊢ req-vec(k - 1;a;b)
BY
{ RepeatFor 2 (ParallelLast) }

1
1. k : ℕ+
2. a : ℝ^k - 1
3. b : ℝ^k - 1
4. z : ℝ
5. u : ℝ
6. ∀i:ℕk. ((a++z i) = (b++u i))
7. i : ℕk - 1
8. (a++z i) = (b++u i)
⊢ (a i) = (b i)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbR{}\^{}k  -  1
3.  b  :  \mBbbR{}\^{}k  -  1
4.  z  :  \mBbbR{}
5.  u  :  \mBbbR{}
6.  req-vec(k;a++z;b++u)
\mvdash{}  req-vec(k  -  1;a;b)


By

---

Latex:
RepeatFor  2  (ParallelLast)

---

Home Index