---

Step * of Lemma fps-product-reindex

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[h:A ⟶ T].
    ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b:bag(T)].  (Π(x∈b).f[x] = Π(x∈bag-map(g;b)).f[h x] ∈ PowerSeries(X;r)) 
    supposing ∀x:T. (x = (h (g x)) ∈ T) 
  supposing valueall-type(X)
BY
{ xxx(Auto
      THEN RepUR ``fps-product bag-product`` 0
      THEN UsingVars [`h'] (BLemma `bag-summation-reindex`)
      THEN Auto
      THEN D 0
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[T,A:Type].  \mforall{}[g:T  {}\mrightarrow{}  A].  \mforall{}[h:A  {}\mrightarrow{}  T].
        \mforall{}[f:T  {}\mrightarrow{}  PowerSeries(X;r)].  \mforall{}[b:bag(T)].    (\mPi{}(x\mmember{}b).f[x]  =  \mPi{}(x\mmember{}bag-map(g;b)).f[h  x]) 
        supposing  \mforall{}x:T.  (x  =  (h  (g  x))) 
    supposing  valueall-type(X)


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``fps-product  bag-product``  0
        THEN  UsingVars  [`h']  (BLemma  `bag-summation-reindex`)
        THEN  Auto
        THEN  D  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index