---

Step * of Lemma oal_dom_neg

∀a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  (dom(--ps) = dom(ps) ∈ FiniteSet{a})
BY
{ ((RepD  
THENM Assert dom(ps) ∈ FiniteSet{a} 
THENM InvertRel 0 
THENM EqTypeCD) THENA Auto) }

1
1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
4. dom(ps) ∈ FiniteSet{a}
⊢ dom(ps) = dom(--ps) ∈ MSet{a}

2
1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
4. dom(ps) ∈ FiniteSet{a}
5. x : |a|
⊢ (x #∈ dom(ps)) ≤ 1

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDGrp.  \mforall{}ps:|oal(a;b)|.    (dom(--ps)  =  dom(ps))


By

---

Latex:
((RepD   
THENM  Assert  dom(ps)  \mmember{}  FiniteSet\{a\} 
THENM  InvertRel  0 
THENM  EqTypeCD)  THENA  Auto)

---

Home Index