---

Step * 1 2 1 1 of Lemma formal-sum-mul_functionality


1. K : CRng
2. k : |K|
3. k1 : |K|
4. k2 : |K|
5. k3 : |K|
⊢ (k * ((k1 +K k2) * k3)) = ((k1 +K k2) * (k * k3)) ∈ |K|
BY
{ (GenConclTerms Auto [⌜k1 +K k2⌝]⋅ THEN RW CRngNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  k  :  |K|
3.  k1  :  |K|
4.  k2  :  |K|
5.  k3  :  |K|
\mvdash{}  (k  *  ((k1  +K  k2)  *  k3))  =  ((k1  +K  k2)  *  (k  *  k3))


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}k1  +K  k2\mkleeneclose{}]\mcdot{}  THEN  RW  CRngNormC  0  THEN  Auto)

---

Home Index