---

Step * of Lemma fps-set-to-one-slice

∀[r:CRng]. ∀[y:Atom]. ∀[n,k:ℕ]. ∀[f:PowerSeries(r)].
  ([[f]_k]_n(y:=1) = if (k =z n) then [f]_n(y:=1) else 0 fi  ∈ PowerSeries(r))
BY
{ (Auto
   THEN (BLemma `fps-ext` THEN Auto)
   THEN RepUR ``fps-zero fps-single fps-slice fps-coeff fps-set-to-one`` 0
   THEN (BoolCase ⌜(k =z n)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN (RWW "bag-size-append bag-size-rep" 0 THENA Auto')
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[y:Atom].  \mforall{}[n,k:\mBbbN{}].  \mforall{}[f:PowerSeries(r)].
    ([[f]\_k]\_n(y:=1)  =  if  (k  =\msubz{}  n)  then  [f]\_n(y:=1)  else  0  fi  )


By

---

Latex:
(Auto
  THEN  (BLemma  `fps-ext`  THEN  Auto)
  THEN  RepUR  ``fps-zero  fps-single  fps-slice  fps-coeff  fps-set-to-one``  0
  THEN  (BoolCase  \mkleeneopen{}(k  =\msubz{}  n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (RWW  "bag-size-append  bag-size-rep"  0  THENA  Auto')
  THEN  AutoSplit)

---

Home Index