---

Step * of Lemma oal_dom_wf2

∀a:LOSet. ∀b:AbDMon. ∀ps:|oal(a;b)|.  (dom(ps) ∈ FiniteSet{a})
BY
{ RepD THENM MemTypeCD THENW Auto }

1
1. a : LOSet@i'
2. b : AbDMon@i'
3. ps : |oal(a;b)|@i
⊢ dom(ps) ∈ MSet{a}

2
.....set predicate..... 
1. a : LOSet@i'
2. b : AbDMon@i'
3. ps : |oal(a;b)|@i
⊢ ∀x:|a|. ((x #∈ dom(ps)) ≤ 1)

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}ps:|oal(a;b)|.    (dom(ps)  \mmember{}  FiniteSet\{a\})


By

---

Latex:
RepD  THENM  MemTypeCD  THENW  Auto

---

Home Index