---

Step * 2 1 of Lemma fps-product-upto


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
7. [1, k) ∈ bag(ℕk)
8. {0} ∈ bag(ℕk)
9. upto(k - 1) ∈ bag(ℕk - 1)
10. {0} + [1, k) ∈ bag(ℕk)
11. ∀[f:ℕk ⟶ PowerSeries(X;r)]. ∀[b,c:bag(ℕk)].  (Π(x∈b + c).f[x] = (Π(x∈b).f[x]*Π(x∈c).f[x]) ∈ PowerSeries(X;r))
⊢ Π(x∈{0}).f[x] = f[0] ∈ PowerSeries(X;r)
BY
{ xxx((InstLemma `fps-product-single` [⌜X⌝;⌜eq⌝;⌜r⌝;⌜ℕk⌝]⋅ THENA Auto) THEN (RWO "-1" 0 THENA Auto) THEN EqCD THEN Auto)
⋅xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  k  :  \mBbbN{}\msupplus{}
6.  f  :  \mBbbN{}k  {}\mrightarrow{}  PowerSeries(X;r)
7.  [1,  k)  \mmember{}  bag(\mBbbN{}k)
8.  \{0\}  \mmember{}  bag(\mBbbN{}k)
9.  upto(k  -  1)  \mmember{}  bag(\mBbbN{}k  -  1)
10.  \{0\}  +  [1,  k)  \mmember{}  bag(\mBbbN{}k)
11.  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  PowerSeries(X;r)].  \mforall{}[b,c:bag(\mBbbN{}k)].    (\mPi{}(x\mmember{}b  +  c).f[x]  =  (\mPi{}(x\mmember{}b).f[x]*\mPi{}(x\mmember{}c).f[x]))
\mvdash{}  \mPi{}(x\mmember{}\{0\}).f[x]  =  f[0]


By

---

Latex:
xxx((InstLemma  `fps-product-single`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mBbbN{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (RWO  "-1"  0  THENA  Auto)
        THEN  EqCD
        THEN  Auto)\mcdot{}xxx

---

Home Index