---

Step * of Lemma algebra_times_one

∀[A:Rng]. ∀[m:algebra{i:l}(A)]. ∀[x:m.car].  (((x m.times m.one) = x ∈ m.car) ∧ ((m.one m.times x) = x ∈ m.car))
BY
{ (Auto THEN AddProperties 2 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Rng].  \mforall{}[m:algebra\{i:l\}(A)].  \mforall{}[x:m.car].    (((x  m.times  m.one)  =  x)  \mwedge{}  ((m.one  m.times  x)  =  x))


By

---

Latex:
(Auto  THEN  AddProperties  2  THEN  Auto)

---

Home Index