---

Step * of Lemma zero-bfs_wf

∀[S:Type]. ∀[K:RngSig]. ∀[ss:bag(S)].  (0 * ss ∈ basic-formal-sum(K;S))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:RngSig].  \mforall{}[ss:bag(S)].    (0  *  ss  \mmember{}  basic-formal-sum(K;S))


By

---

Latex:
ProveWfLemma

---

Home Index