---

Step * 1 of Lemma omral_fact_a


∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (ps = (msFor{oal_mon(g↓oset;r↓+gp)} k' ∈ dom(ps). inj(k',ps[k'])) ∈ |omral(g;r)|)
BY
{ Lemma `omral_fact` }

---

Latex:

---

Latex:

\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps:|omral(g;r)|.
    (ps  =  (msFor\{oal\_mon(g\mdownarrow{}oset;r\mdownarrow{}+gp)\}  k'  \mmember{}  dom(ps).  inj(k',ps[k'])))


By

---

Latex:
Lemma  `omral\_fact`

---

Home Index