---

Step * of Lemma fps-compose-identity

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[x:X].  (f(x:=atom(x)) = f ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN ((InstLemma `fps-linear-ucont-equal` [⌜X⌝;⌜eq⌝;⌜r⌝;⌜λ2f.f(x:=atom(x))⌝;⌜λ2f.f⌝]⋅
         THENM ((ApFunToHypEquands `Z' ⌜Z[f]⌝ ⌜PowerSeries(X;r)⌝ (-1)⋅ THEN Auto)
                THEN RepUR ``so_apply so_lambda`` -1
                THEN Auto)
         )
         THENA (Auto
                THEN (Try ((BLemma `fps-compose-ucont` THEN Auto)) THEN Try ((BLemma `fps-id-ucont` THEN Auto)))
                THEN RWW "fps-compose-add fps-compose-scalar-mul" 0
                THEN Auto)
         )
   ) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. x : X
7. fps-ucont(X;eq;r;f.f(x:=atom(x)))
8. fps-ucont(X;eq;r;f.f)
9. ∀f,g:PowerSeries(X;r).  ((f+g)(x:=atom(x)) = (f(x:=atom(x))+g(x:=atom(x))) ∈ PowerSeries(X;r))
10. ∀f,g:PowerSeries(X;r).  ((f+g) = (f+g) ∈ PowerSeries(X;r))
11. ∀c:|r|. ∀f:PowerSeries(X;r).  ((c)*f(x:=atom(x)) = (c)*f(x:=atom(x)) ∈ PowerSeries(X;r))
12. ∀c:|r|. ∀f:PowerSeries(X;r).  ((c)*f = (c)*f ∈ PowerSeries(X;r))
13. b : bag(X)
⊢ <b>(x:=atom(x)) = <b> ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f:PowerSeries(X;r)].  \mforall{}[x:X].    (f(x:=atom(x))  =  f) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  ((InstLemma  `fps-linear-ucont-equal`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.f(x:=atom(x))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.f\mkleeneclose{}]\mcdot{}
              THENM  ((ApFunToHypEquands  `Z'  \mkleeneopen{}Z[f]\mkleeneclose{}  \mkleeneopen{}PowerSeries(X;r)\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)
                            THEN  RepUR  ``so\_apply  so\_lambda``  -1
                            THEN  Auto)
              )
              THENA  (Auto
                            THEN  (Try  ((BLemma  `fps-compose-ucont`  THEN  Auto))
                                        THEN  Try  ((BLemma  `fps-id-ucont`  THEN  Auto))
                                        )
                            THEN  RWW  "fps-compose-add  fps-compose-scalar-mul"  0
                            THEN  Auto)
              )
  )

---

Home Index