---

Step * of Lemma fps-compose-single

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[b:bag(X)]. ∀[f:PowerSeries(X;r)].
    <b>(x:=f) = (<(b|¬x)>*(f)^(#((b|x)))) ∈ PowerSeries(X;r) supposing f[{}] = 0 ∈ |r| 
  supposing valueall-type(X)
BY
{ xxx(Auto THEN (RWO "fps-compose-single-general" 0 THENA Auto) THEN RepeatFor 2 ((EqCDA THEN Auto)))xxx }

1
.....subterm..... T:t
4:n
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. b : bag(X)
7. f : PowerSeries(X;r)
8. f[{}] = 0 ∈ |r|
⊢ (f-(f[{}])*1) = f ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].  \mforall{}[b:bag(X)].  \mforall{}[f:PowerSeries(X;r)].
        <b>(x:=f)  =  (<(b|\mneg{}x)>*(f)\^{}(\#((b|x))))  supposing  f[\{\}]  =  0 
    supposing  valueall-type(X)


By

---

Latex:
xxx(Auto
        THEN  (RWO  "fps-compose-single-general"  0  THENA  Auto)
        THEN  RepeatFor  2  ((EqCDA  THEN  Auto)))xxx

---

Home Index