---

Step * of Lemma fps-elim-x-one

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X].  (1(x:=0) = 1 ∈ PowerSeries(X;r))
BY
{ (Auto
   THEN BLemma `fps-ext`
   THEN Auto
   THEN RepUR ``fps-elim-x fps-elim fps-one fps-coeff`` 0
   THEN RepeatFor 2 (AutoSplit)) }

1
1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. x : X
5. b : bag(X)
6. x ↓∈ b
7. b = {} ∈ bag(X)
⊢ 0 = 1 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].    (1(x:=0)  =  1)


By

---

Latex:
(Auto
  THEN  BLemma  `fps-ext`
  THEN  Auto
  THEN  RepUR  ``fps-elim-x  fps-elim  fps-one  fps-coeff``  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index