---

Step * of Lemma rng_times_assoc

∀[r:Rng]. ∀[a,b,c:|r|].  ((a * (b * c)) = ((a * b) * c) ∈ |r|)
BY
{ ProveSpecializedLemma `mon_assoc` 1 [parm{i};r↓xmn] (AbReduceC) }

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b,c:|r|].    ((a  *  (b  *  c))  =  ((a  *  b)  *  c))


By

---

Latex:
ProveSpecializedLemma  `mon\_assoc`  1  [parm\{i\};r\mdownarrow{}xmn]  (AbReduceC)

---

Home Index