---

Step * 1 of Lemma fps-pascal-slice


1. r : CRng
2. x : Atom
3. y : Atom
⊢ [(<{x}>+<{y}>)]_1 = (<{x}>+<{y}>) ∈ PowerSeries(r)
BY
{ xxx((RWW "fps-add-slice fps-single-slice" 0 THEN Auto) THEN RepUR ``bag-size single-bag`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
\mvdash{}  [(<\{x\}>+<\{y\}>)]\_1  =  (<\{x\}>+<\{y\}>)


By

---

Latex:
xxx((RWW  "fps-add-slice  fps-single-slice"  0  THEN  Auto)
        THEN  RepUR  ``bag-size  single-bag``  0
        THEN  Auto)xxx

---

Home Index