---

Step * 1 of Lemma oal_dom_neg


1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
4. dom(ps) ∈ FiniteSet{a}
⊢ dom(ps) = dom(--ps) ∈ MSet{a}
BY
{ ((Thin 4 THEN Unfold `oal_dom` 0 
THENM RW mset_elimC 0) THENA Auto) }

1
1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
⊢ map(λz.(fst(z));ps) ≡(|a|) map(λz.(fst(z));--ps)

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDGrp
3.  ps  :  |oal(a;b)|
4.  dom(ps)  \mmember{}  FiniteSet\{a\}
\mvdash{}  dom(ps)  =  dom(--ps)


By

---

Latex:
((Thin  4  THEN  Unfold  `oal\_dom`  0 
THENM  RW  mset\_elimC  0)  THENA  Auto)

---

Home Index