---

Step * of Lemma negerse_fps

∀[X:Type]. ∀[r:CRng]. ∀[a:PowerSeries(X;r)].  (((a+-(a)) = 0 ∈ PowerSeries(X;r)) ∧ ((-(a)+a) = 0 ∈ PowerSeries(X;r)))
BY
{ xxxAutoxxx }

1
1. X : Type
2. r : CRng
3. a : PowerSeries(X;r)
⊢ (a+-(a)) = 0 ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[a:PowerSeries(X;r)].    (((a+-(a))  =  0)  \mwedge{}  ((-(a)+a)  =  0))


By

---

Latex:
xxxAutoxxx

---

Home Index