---

Step * 1 1 1 of Lemma omral_times_ident_l


1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. u : |g|
⊢ ((inj(e,1) ** ps)[u]) = (ps[u]) ∈ |r|
BY
{ (RWW "lookup_omral_times omral_dom_inj" 0) THENA Auto }

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

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  ps  :  |omral(g;r)|
4.  u  :  |g|
\mvdash{}  ((inj(e,1)  **  ps)[u])  =  (ps[u])


By

---

Latex:
(RWW  "lookup\_omral\_times  omral\_dom\_inj"  0)  THENA  Auto

---

Home Index