---

Step * 3 1 of Lemma fps-mul-coeff-bag-rep-simple


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. bag-no-repeats(bag(X) × bag(X);bag-partitions(eq;bag-rep(n;x)))
⊢ (bag-rep(k;x) + bag-rep(n - k;x)) = bag-rep(n;x) ∈ bag(X)
BY
{ (RWO "bag-append-equal-bag-rep" 0 THEN Auto)⋅ }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. bag-no-repeats(bag(X) × bag(X);bag-partitions(eq;bag-rep(n;x)))
⊢ n = (#(bag-rep(k;x)) + #(bag-rep(n - k;x))) ∈ ℤ

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  n  :  \mBbbN{}
5.  k  :  \mBbbN{}n  +  1
6.  r  :  CRng
7.  f  :  PowerSeries(X;r)
8.  g  :  PowerSeries(X;r)
9.  x  :  X
10.  \mforall{}i:\mBbbN{}n  +  1.  ((\mneg{}(i  =  k))  {}\mRightarrow{}  (f[bag-rep(i;x)]  =  0))
11.  bag-no-repeats(bag(X)  \mtimes{}  bag(X);bag-partitions(eq;bag-rep(n;x)))
\mvdash{}  (bag-rep(k;x)  +  bag-rep(n  -  k;x))  =  bag-rep(n;x)


By

---

Latex:
(RWO  "bag-append-equal-bag-rep"  0  THEN  Auto)\mcdot{}

---

Home Index