---

Step * of Lemma power-vs-sq

∀[K,S:Top].  (K^S ~ Point= S ⟶ |K| zero= λs.0 a+b= λs.((a s) +K (b s)) a*b= λs.(a * (b s)))
BY
{ (Auto
   THEN RepUR ``power-vs vs-exp vs-sum`` 0
   THEN EqCD
   THEN RepUR ``one-dim-vs vs-point mk-vs vs-0 vs-add vs-mul`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K,S:Top].    (K\^{}S  \msim{}  Point=  S  {}\mrightarrow{}  |K|  zero=  \mlambda{}s.0  a+b=  \mlambda{}s.((a  s)  +K  (b  s))  a*b=  \mlambda{}s.(a  *  (b  s)))


By

---

Latex:
(Auto
  THEN  RepUR  ``power-vs  vs-exp  vs-sum``  0
  THEN  EqCD
  THEN  RepUR  ``one-dim-vs  vs-point  mk-vs  vs-0  vs-add  vs-mul``  0
  THEN  Auto)

---

Home Index