---

Step * 1 5 of Lemma oal_grp_wf


1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ IsEqFun(|oal(s;g)|;=b)
BY
{ ((Assert ⌜oal(s;g) ∈ DSet⌝⋅ THENM AddProperties (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  AbDGrp@i'
\mvdash{}  IsEqFun(|oal(s;g)|;=\msubb{})


By

---

Latex:
((Assert  \mkleeneopen{}oal(s;g)  \mmember{}  DSet\mkleeneclose{}\mcdot{}  THENM  AddProperties  (-1))  THEN  Auto)

---

Home Index