---

Step * of Lemma mul_mon_of_rng_wf_b

∀[r:CRng]. (r↓xmn ∈ AbMon)
BY
{ ((D 0 
THENM AddAllProperties 1 
) THENA Auto) }

1
1. r : CRng
2. Assoc(|r|;+r)
3. Ident(|r|;+r;0)
4. Inverse(|r|;+r;0;-r)
5. Assoc(|r|;*)
6. Comm(|r|;*)
7. Ident(|r|;*;1)
8. BiLinear(|r|;+r;*)
⊢ r↓xmn ∈ AbMon

---

Latex:

---

Latex:
\mforall{}[r:CRng].  (r\mdownarrow{}xmn  \mmember{}  AbMon)


By

---

Latex:
((D  0 
THENM  AddAllProperties  1 
)  THENA  Auto)

---

Home Index