---

Step * of Lemma fps-elim-hom

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X].
    (FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f+g);λf,g. (f+g);fps-elim(x))
    ∧ FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f*g);λf,g. (f*g);fps-elim(x))
    ∧ ((fps-elim(x) 1) = 1 ∈ PowerSeries(X;r))) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN Try (Complete (((BLemma `fps-ext` THEN Auto)
                        THEN RepUR ``fps-one fps-elim fps-coeff`` 0
                        THEN RepeatFor 2 (AutoSplit)
                        THEN HypSubst' (-1) (-2)
                        THEN Auto
                        THEN BagMemberD (-2))))
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN BLemma `fps-ext`
   THEN Auto
   THEN RepUR ``fps-elim fps-add fps-mul fps-coeff`` 0
   THEN AutoSplit
   THEN RW RngNormC 0
   THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f+g);λf,g. (f+g);fps-elim(x))
7. a1 : PowerSeries(X;r)
8. a2 : PowerSeries(X;r)
9. b : bag(X)
10. x ↓∈ b
⊢ 0
= Σ(p∈bag-partitions(eq;b)). * if bag-deq-member(eq;x;fst(p)) then 0 else a1 (fst(p)) fi  
                             if bag-deq-member(eq;x;snd(p)) then 0 else a2 (snd(p)) fi 
∈ |r|

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f+g);λf,g. (f+g);fps-elim(x))
7. a1 : PowerSeries(X;r)
8. a2 : PowerSeries(X;r)
9. b : bag(X)
10. ¬x ↓∈ b
⊢ Σ(p∈bag-partitions(eq;b)). * (a1 (fst(p))) (a2 (snd(p)))
= Σ(p∈bag-partitions(eq;b)). * if bag-deq-member(eq;x;fst(p)) then 0 else a1 (fst(p)) fi  
                             if bag-deq-member(eq;x;snd(p)) then 0 else a2 (snd(p)) fi 
∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].
        (FunThru2op(PowerSeries(X;r);PowerSeries(X;r);\mlambda{}f,g.  (f+g);\mlambda{}f,g.  (f+g);fps-elim(x))
        \mwedge{}  FunThru2op(PowerSeries(X;r);PowerSeries(X;r);\mlambda{}f,g.  (f*g);\mlambda{}f,g.  (f*g);fps-elim(x))
        \mwedge{}  ((fps-elim(x)  1)  =  1)) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  Try  (Complete  (((BLemma  `fps-ext`  THEN  Auto)
                                            THEN  RepUR  ``fps-one  fps-elim  fps-coeff``  0
                                            THEN  RepeatFor  2  (AutoSplit)
                                            THEN  HypSubst'  (-1)  (-2)
                                            THEN  Auto
                                            THEN  BagMemberD  (-2))))
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  BLemma  `fps-ext`
  THEN  Auto
  THEN  RepUR  ``fps-elim  fps-add  fps-mul  fps-coeff``  0
  THEN  AutoSplit
  THEN  RW  RngNormC  0
  THEN  Auto)

---

Home Index