---

Step * of Lemma module_plus_inv

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

---

Latex:

---

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


By

---

Latex:
(ProvePropertyLemma  `inverse`  2  THEN  Auto)

---

Home Index