---

Step * of Lemma integral_functionality_endpoints

∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
  ∀a',b':ℝ.  (a_∫-b f[x] dx = a'_∫-b' f[x] dx) supposing ((a = a') and (b = b'))
BY
{ (Auto THEN Try ((RWO "6 7" 0 THEN Auto))) }

1
1. a : ℝ
2. b : ℝ
3. f : {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} 
4. a' : ℝ
5. b' : ℝ
6. b = b'
7. a = a'
⊢ a_∫-b f[x] dx = a'_∫-b' f[x] dx

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].  \mforall{}[f:\{f:[rmin(a;b),  rmax(a;b)]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[rmin(a;b),  rmax(a;b)])\}  ].
    \mforall{}a',b':\mBbbR{}.    (a\_\mint{}\msupminus{}b  f[x]  dx  =  a'\_\mint{}\msupminus{}b'  f[x]  dx)  supposing  ((a  =  a')  and  (b  =  b'))


By

---

Latex:
(Auto  THEN  Try  ((RWO  "6  7"  0  THEN  Auto)))

---

Home Index