---

Step * of Lemma rfun*_functionality

∀[f:ℝ ⟶ ℝ]. ∀[x,y:ℝ*].  ((∀[a,b:ℝ].  (f a) = (f b) supposing a = b) ⇒ x = y ⇒ f*(x) = f*(y))
BY
{ (Auto THEN RepeatFor 3 (ParallelLast) THEN RepUR ``rfun*`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x,y:\mBbbR{}*].    ((\mforall{}[a,b:\mBbbR{}].    (f  a)  =  (f  b)  supposing  a  =  b)  {}\mRightarrow{}  x  =  y  {}\mRightarrow{}  f*(x)  =  f*(y))


By

---

Latex:
(Auto  THEN  RepeatFor  3  (ParallelLast)  THEN  RepUR  ``rfun*``  0  THEN  Auto)

---

Home Index