---

Step * 1 1 1 1 2 of Lemma omral_times_ident_l

.....falsecase..... 
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. u : |g|
5. ¬(1 = 0 ∈ |r|)
⊢ (msFor{r↓+gp} x ∈ mset_inj{g↓oset}(e)
     msFor{r↓+gp} y ∈ dom(ps)
       when (x * y) =b u.
         ((inj(e,1)[x]) * (ps[y])))
= (ps[u])
∈ |r|
BY
{ ((RWW "mset_for_mset_inj" 0 
THENM RW MonNormC 0) THENA Auto) }

1
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. u : |g|
5. ¬(1 = 0 ∈ |r|)
⊢ (msFor{r↓+gp} y ∈ dom(ps). when y =b u. ((inj(e,1)[e]) * (ps[y]))) = (ps[u]) ∈ |r|

---

Latex:

---

Latex:
.....falsecase..... 
1.  g  :  OCMon
2.  r  :  CDRng
3.  ps  :  |omral(g;r)|
4.  u  :  |g|
5.  \mneg{}(1  =  0)
\mvdash{}  (msFor\{r\mdownarrow{}+gp\}  x  \mmember{}  mset\_inj\{g\mdownarrow{}oset\}(e)
          msFor\{r\mdownarrow{}+gp\}  y  \mmember{}  dom(ps)
              when  (x  *  y)  =\msubb{}  u.
                  ((inj(e,1)[x])  *  (ps[y])))
=  (ps[u])


By

---

Latex:
((RWW  "mset\_for\_mset\_inj"  0 
THENM  RW  MonNormC  0)  THENA  Auto)

---

Home Index