---

Step * of Lemma zero-bfs-append

∀[S:Type]. ∀[K:RngSig]. ∀[ss1,ss2:bag(S)].  (0 * ss1 + ss2 = (0 * ss1 + 0 * ss2) ∈ basic-formal-sum(K;S))
BY
{ ((Auto THEN Unfold `zero-bfs` 0) THEN Unfold `basic-formal-sum` 0 THEN RWO "bag-map-append" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:RngSig].  \mforall{}[ss1,ss2:bag(S)].    (0  *  ss1  +  ss2  =  (0  *  ss1  +  0  *  ss2))


By

---

Latex:
((Auto  THEN  Unfold  `zero-bfs`  0)
  THEN  Unfold  `basic-formal-sum`  0
  THEN  RWO  "bag-map-append"  0
  THEN  Auto)

---

Home Index