---

Step * of Lemma algebra_act_times_r

∀[A:Rng]. ∀[m:algebra{i:l}(A)]. ∀[a:|A|]. ∀[u,v:m.car].
  (((m.act a (u m.times v)) = ((m.act a u) m.times v) ∈ m.car)
  ∧ ((m.act a (u m.times v)) = (u m.times (m.act a v)) ∈ m.car))
BY
{ (Auto THEN AddProperties 2 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Rng].  \mforall{}[m:algebra\{i:l\}(A)].  \mforall{}[a:|A|].  \mforall{}[u,v:m.car].
    (((m.act  a  (u  m.times  v))  =  ((m.act  a  u)  m.times  v))
    \mwedge{}  ((m.act  a  (u  m.times  v))  =  (u  m.times  (m.act  a  v))))


By

---

Latex:
(Auto  THEN  AddProperties  2  THEN  Auto)

---

Home Index