---

Step * 1 of Lemma radd*_functionality


1. [x] : ℝ*
2. [y] : ℝ*
3. [u] : ℝ*
4. [v] : ℝ*
5. x = y
6. u = v
⊢ λa,b. (a + b)*(y;v) = λa,b. (a + b)*(y;v)
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  [x]  :  \mBbbR{}*
2.  [y]  :  \mBbbR{}*
3.  [u]  :  \mBbbR{}*
4.  [v]  :  \mBbbR{}*
5.  x  =  y
6.  u  =  v
\mvdash{}  \mlambda{}a,b.  (a  +  b)*(y;v)  =  \mlambda{}a,b.  (a  +  b)*(y;v)


By

---

Latex:
EAuto  1

---

Home Index