---

Step * of Lemma fps-non-trivial

∀[X:Type]. ∀[r:CRng].  ¬(1 = 0 ∈ PowerSeries(X;r)) supposing ¬(1 = 0 ∈ |r|)
BY
{ xxx(Auto THEN ParallelLast THEN (Assert 1[{}] = 0[{}] ∈ |r| BY Auto))xxx }

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

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].    \mneg{}(1  =  0)  supposing  \mneg{}(1  =  0)


By

---

Latex:
xxx(Auto  THEN  ParallelLast  THEN  (Assert  1[\{\}]  =  0[\{\}]  BY  Auto))xxx

---

Home Index