---

Step * of Lemma oal_nil_ident_l

∀a:LOSet. ∀b:AbDMon. ∀ps:|oal(a;b)|.  ((00 ++ ps) = ps ∈ |oal(a;b)|)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}ps:|oal(a;b)|.    ((00  ++  ps)  =  ps)


By

---

Latex:
Auto

---

Home Index