---

Step * of Lemma fps-linear-ucont-equal

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[F,G:PowerSeries(X;r) ⟶ PowerSeries(X;r)].
    F = G ∈ (PowerSeries(X;r) ⟶ PowerSeries(X;r)) 
    supposing fps-ucont(X;eq;r;f.F[f])
    ∧ fps-ucont(X;eq;r;f.G[f])
    ∧ (∀f,g:PowerSeries(X;r).  (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r)))
    ∧ (∀f,g:PowerSeries(X;r).  (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r)))
    ∧ (∀c:|r|. ∀f:PowerSeries(X;r).  (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r)))
    ∧ (∀c:|r|. ∀f:PowerSeries(X;r).  (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r)))
    ∧ (∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN Ext
   THEN Auto
   THEN RenameVar `f' (-1)
   THEN BLemma `fps-ext`
   THEN Auto
   THEN (RepeatFor 2 ((With ⌜b⌝ (D 7)⋅ THENA Auto)) THEN ExRepD)
   THEN RWO "-3 -1" 0
   THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. F : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
7. ∀f,g:PowerSeries(X;r).  (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r))
8. ∀f,g:PowerSeries(X;r).  (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r))
9. ∀c:|r|. ∀f:PowerSeries(X;r).  (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r))
10. ∀c:|r|. ∀f:PowerSeries(X;r).  (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r))
11. ∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
16. d : bag(X)
17. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
⊢ F[fps-restrict(eq;r;f;d1)][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[F,G:PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r)].
        F  =  G 
        supposing  fps-ucont(X;eq;r;f.F[f])
        \mwedge{}  fps-ucont(X;eq;r;f.G[f])
        \mwedge{}  (\mforall{}f,g:PowerSeries(X;r).    (F[(f+g)]  =  (F[f]+F[g])))
        \mwedge{}  (\mforall{}f,g:PowerSeries(X;r).    (G[(f+g)]  =  (G[f]+G[g])))
        \mwedge{}  (\mforall{}c:|r|.  \mforall{}f:PowerSeries(X;r).    (F[(c)*f]  =  (c)*F[f]))
        \mwedge{}  (\mforall{}c:|r|.  \mforall{}f:PowerSeries(X;r).    (G[(c)*f]  =  (c)*G[f]))
        \mwedge{}  (\mforall{}b:bag(X).  (F[<b>]  =  G[<b>])) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  Ext
  THEN  Auto
  THEN  RenameVar  `f'  (-1)
  THEN  BLemma  `fps-ext`
  THEN  Auto
  THEN  (RepeatFor  2  ((With  \mkleeneopen{}b\mkleeneclose{}  (D  7)\mcdot{}  THENA  Auto))  THEN  ExRepD)
  THEN  RWO  "-3  -1"  0
  THEN  Auto)

---

Home Index