---

Step * of Lemma omral_dom_wf2

∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (dom(ps) ∈ FiniteSet{g↓oset})
BY
{ (Auto THEN Unfold `omral_dom` 0 THEN BLemma `oal_dom_wf2` THEN Auto THEN (BLemma `cdrng_is_abdmonoid` THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps:|omral(g;r)|.    (dom(ps)  \mmember{}  FiniteSet\{g\mdownarrow{}oset\})


By

---

Latex:
(Auto
  THEN  Unfold  `omral\_dom`  0
  THEN  BLemma  `oal\_dom\_wf2`
  THEN  Auto
  THEN  (BLemma  `cdrng\_is\_abdmonoid`  THEN  Auto)\mcdot{})

---

Home Index