---

Step * of Lemma mul-one

∀[x:ℤ]. (x * 1 ~ x)
BY
{ ((UnivCD THENA Auto) THEN (RWO "mul-commutes" 0 THENA Trivial) THEN RWO "one-mul" 0 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (x  *  1  \msim{}  x)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "mul-commutes"  0  THENA  Trivial)  THEN  RWO  "one-mul"  0  THEN  Trivial)

---

Home Index