---

Step * 1 of Lemma omral_dom_one


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}
BY
{ ((SplitOnConclITE THENA Auto) THEN (RelRST THEN Auto)) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  \mneg{}(0  =  1)
\mvdash{}  if  1  =\msubb{}  0  then  0\{g\mdownarrow{}oset\}  else  mset\_inj\{g\mdownarrow{}oset\}(e)  fi    =  mset\_inj\{g\mdownarrow{}oset\}(e)


By

---

Latex:
((SplitOnConclITE  THENA  Auto)  THEN  (RelRST  THEN  Auto))

---

Home Index