---

Step * of Lemma fps-product-upto

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[k:ℕ+]. ∀[f:ℕk ⟶ PowerSeries(X;r)].
    (Π(x∈upto(k)).f[x] = (f[0]*Π(x∈upto(k - 1)).f[x + 1]) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ xxx(Auto THEN Subst' upto(k) ~ {0} + [1, k) 0⋅)xxx }

1
.....equality..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
⊢ upto(k) ~ {0} + [1, k)

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
⊢ Π(x∈{0} + [1, k)).f[x] = (f[0]*Π(x∈upto(k - 1)).f[x + 1]) ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  PowerSeries(X;r)].
        (\mPi{}(x\mmember{}upto(k)).f[x]  =  (f[0]*\mPi{}(x\mmember{}upto(k  -  1)).f[x  +  1])) 
    supposing  valueall-type(X)


By

---

Latex:
xxx(Auto  THEN  Subst'  upto(k)  \msim{}  \{0\}  +  [1,  k)  0\mcdot{})xxx

---

Home Index