---

Step * 4 1 1 of Lemma alg_act_is_rng_chom


1. a : CRng
2. m : algebra{i:l}(a)
3. a@0 : |a|
4. b : |a|
⊢ ((a@0 * b) m.act m.one) = ((b * a@0) m.act m.one) ∈ m.car
BY
{ ((RW CRngNormC 0) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  CRng
2.  m  :  algebra\{i:l\}(a)
3.  a@0  :  |a|
4.  b  :  |a|
\mvdash{}  ((a@0  *  b)  m.act  m.one)  =  ((b  *  a@0)  m.act  m.one)


By

---

Latex:
((RW  CRngNormC  0)  THEN  Auto)

---

Home Index