---

Step * 1 of Lemma fps-non-trivial


1. X : Type
2. r : CRng
3. 1 = 0 ∈ PowerSeries(X;r)
4. 1[{}] = 0[{}] ∈ |r|
⊢ 1 = 0 ∈ |r|
BY
{ (FpsCompute (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  r  :  CRng
3.  1  =  0
4.  1[\{\}]  =  0[\{\}]
\mvdash{}  1  =  0


By

---

Latex:
(FpsCompute  (-1)  THEN  Auto)

---

Home Index