---

Step * of Lemma omral_dom_one

∀g:OCMon. ∀r:CDRng.  ((¬(0 = 1 ∈ |r|)) ⇒ (dom(11) = mset_inj{g↓oset}(e) ∈ FiniteSet{g↓oset}))
BY
{ (RepD THENM RWW "u:omral_one omral_dom_inj" 0) THENA Auto⋅ }

1
1. g : OCMon
2. r : CDRng
3. ¬(0 = 1 ∈ |r|)
⊢ if 1 =b 0 then 0{g↓oset} else mset_inj{g↓oset}(e) fi  = mset_inj{g↓oset}(e) ∈ FiniteSet{g↓oset}

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.    ((\mneg{}(0  =  1))  {}\mRightarrow{}  (dom(11)  =  mset\_inj\{g\mdownarrow{}oset\}(e)))


By

---

Latex:
(RepD  THENM  RWW  "u:omral\_one  omral\_dom\_inj"  0)  THENA  Auto\mcdot{}

---

Home Index