---

Step * of Lemma trivial-null-formal-sum

∀K:Rng. ∀[S:Type]. ∀fs:basic-formal-sum(K;S). null-formal-sum(K;S;fs + -(fs))
BY
{ (Auto THEN (D 0 With ⌜fs⌝  THEN Auto) THEN D 0 With ⌜{}⌝  THEN Auto THEN RepUR ``zero-bfs`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}K:Rng.  \mforall{}[S:Type].  \mforall{}fs:basic-formal-sum(K;S).  null-formal-sum(K;S;fs  +  -(fs))


By

---

Latex:
(Auto
  THEN  (D  0  With  \mkleeneopen{}fs\mkleeneclose{}    THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}\{\}\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``zero-bfs``  0
  THEN  Auto)

---

Home Index