---

Step * of Lemma fps-compose-atom

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x,y:X]. ∀[f:PowerSeries(X;r)].
    atom(y)(x:=f) = if eq y x then f else atom(y) fi  ∈ PowerSeries(X;r) supposing f[{}] = 0 ∈ |r| 
  supposing valueall-type(X)
BY
{ (Auto THEN AutoSplit) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. y : X
7. f : PowerSeries(X;r)
8. f[{}] = 0 ∈ |r|
9. y = x ∈ X
⊢ atom(y)(x:=f) = f ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x,y:X].  \mforall{}[f:PowerSeries(X;r)].
        atom(y)(x:=f)  =  if  eq  y  x  then  f  else  atom(y)  fi    supposing  f[\{\}]  =  0 
    supposing  valueall-type(X)


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index