---

Step * of Lemma module_action_p

∀[A:Rng]. ∀[m:A-Module].
  ((∀[a,b:|A|]. ∀[u:m.car].  (((a * b) m.act u) = (a m.act (b m.act u)) ∈ m.car))
  ∧ (∀[u:m.car]. ((1 m.act u) = u ∈ m.car)))
BY
{ (Auto THEN AddProperties 2 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Rng].  \mforall{}[m:A-Module].
    ((\mforall{}[a,b:|A|].  \mforall{}[u:m.car].    (((a  *  b)  m.act  u)  =  (a  m.act  (b  m.act  u))))
    \mwedge{}  (\mforall{}[u:m.car].  ((1  m.act  u)  =  u)))


By

---

Latex:
(Auto  THEN  AddProperties  2  THEN  Auto)

---

Home Index