---

Step * 2 1 of Lemma req-vec-extend


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)
BY
{ (RepUR ``real-vec-extend`` -1 THEN SplitOnHypITE -1  THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbR{}\^{}k  -  1
3.  b  :  \mBbbR{}\^{}k  -  1
4.  z  :  \mBbbR{}
5.  u  :  \mBbbR{}
6.  \mforall{}i:\mBbbN{}k.  ((a++z  i)  =  (b++u  i))
7.  i  :  \mBbbN{}k  -  1
8.  (a++z  i)  =  (b++u  i)
\mvdash{}  (a  i)  =  (b  i)


By

---

Latex:
(RepUR  ``real-vec-extend``  -1  THEN  SplitOnHypITE  -1    THEN  Auto)

---

Home Index