---

Step * of Lemma omral_fact_a

∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (ps = (msFor{omral_alg(g;r)↓grp} k' ∈ dom(ps). inj(k',ps[k'])) ∈ |omral(g;r)|)
BY
{ % Uggh ! % 
RWH (MacroC `x`  
  (EvalC ``mset_for mon_for``  
   ANDTHENC UnfoldsC ``omral_plus omral_zero``) msFor{omral_alg(g;r)↓grp} x ∈ a
                                                  f[x] 
   (EvalC ``mset_for mon_for``) 
  msFor{oal_mon(g↓oset;r↓+gp)} x ∈ a
    f[x]) 0 
 }

1
∀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)|)

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps:|omral(g;r)|.
    (ps  =  (msFor\{omral\_alg(g;r)\mdownarrow{}grp\}  k'  \mmember{}  dom(ps).  inj(k',ps[k'])))


By

---

Latex:
\%  Uggh  !  \% 
RWH  (MacroC  `x`   
    (EvalC  ``mset\_for  mon\_for``   
      ANDTHENC  UnfoldsC  ``omral\_plus  omral\_zero``)  msFor\{omral\_alg(g;r)\mdownarrow{}grp\}  x  \mmember{}  a
                                                                                                    f[x] 
      (EvalC  ``mset\_for  mon\_for``) 
    msFor\{oal\_mon(g\mdownarrow{}oset;r\mdownarrow{}+gp)\}  x  \mmember{}  a
        f[x])  0 

---

Home Index