---

Step * 1 of Lemma grp_of_module_wf2


1. a : RngSig@i'
2. m : a-Module@i'
⊢ m↓grp ∈ AbGrp
BY
{ ((AddAllProperties 2 
THENM ARepD ["compound"] 
THENM RepeatM MemTypeCD 
THEN IfLabL [`set predicate`, 
  Reduce 0 THEN AGenRepD ["compound"]]) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  RngSig@i'
2.  m  :  a-Module@i'
\mvdash{}  m\mdownarrow{}grp  \mmember{}  AbGrp


By

---

Latex:
((AddAllProperties  2 
THENM  ARepD  ["compound"] 
THENM  RepeatM  MemTypeCD 
THEN  IfLabL  [`set  predicate`, 
    Reduce  0  THEN  AGenRepD  ["compound"]])  THEN  Auto)

---

Home Index