---

Step * of Lemma module_plus_ident

∀[A:Rng]. ∀[m:A-Module]. ∀[x:m.car].  (((x m.plus m.zero) = x ∈ m.car) ∧ ((m.zero m.plus x) = x ∈ m.car))
BY
{ ((ProvePropertyLemma `ident` 2) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Rng].  \mforall{}[m:A-Module].  \mforall{}[x:m.car].    (((x  m.plus  m.zero)  =  x)  \mwedge{}  ((m.zero  m.plus  x)  =  x))


By

---

Latex:
((ProvePropertyLemma  `ident`  2)  THEN  Auto)

---

Home Index