---

Step * of Lemma mul_mon_of_rng_wf_a

∀[r:Rng]. (r↓xmn ∈ Mon)
BY
{ Unfold `mul_mon_of_rng` 0 
THEN ((D 0) THENA Auto) }

1
1. r : Rng
⊢ <|r|, =b, ≤b, *, 1, λz.z> ∈ Mon

---

Latex:

---

Latex:
\mforall{}[r:Rng].  (r\mdownarrow{}xmn  \mmember{}  Mon)


By

---

Latex:
Unfold  `mul\_mon\_of\_rng`  0 
THEN  ((D  0)  THENA  Auto)

---

Home Index