---

Step * 1 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)
⊢ z = u
BY
{ ((D -1 With ⌜k - 1⌝  THENA Auto) THEN 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.  req-vec(k;a++z;b++u)
\mvdash{}  z  =  u


By

---

Latex:
((D  -1  With  \mkleeneopen{}k  -  1\mkleeneclose{}    THENA  Auto)  THEN  RepUR  ``real-vec-extend``  -1  THEN  SplitOnHypITE  -1    THEN  Auto)

---

Home Index