---

Step * of Lemma mon_ident_fps

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

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

---

Latex:

---

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


By

---

Latex:
xxxAutoxxx

---

Home Index