---

Step * of Lemma mul_mon_of_rng_wf

∀[r:RngSig]. (r↓xmn ∈ GrpSig)
BY
{ Unfolds ``mul_mon_of_rng grp_sig`` 0 THEN Auto⋅ }

---

Latex:

---

Latex:
\mforall{}[r:RngSig].  (r\mdownarrow{}xmn  \mmember{}  GrpSig)


By

---

Latex:
Unfolds  ``mul\_mon\_of\_rng  grp\_sig``  0  THEN  Auto\mcdot{}

---

Home Index