---

Step * 2 1 of Lemma alg_act_is_rng_chom


1. a : CRng
2. m : algebra{i:l}(a)
3. a1 : |a|
4. a2 : |a|
⊢ (m.act (a1 * a2) m.one) = (m.act a1 (m.one m.times (m.act a2 m.one))) ∈ m.car
BY
{ ((RWW "module_action_p.1 algebra_times_one.2" 0) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  CRng
2.  m  :  algebra\{i:l\}(a)
3.  a1  :  |a|
4.  a2  :  |a|
\mvdash{}  (m.act  (a1  *  a2)  m.one)  =  (m.act  a1  (m.one  m.times  (m.act  a2  m.one)))


By

---

Latex:
((RWW  "module\_action\_p.1  algebra\_times\_one.2"  0)  THEN  Auto)

---

Home Index