---

Step * of Lemma one-mul

∀[x:ℤ]. (1 * x ~ x)
BY
{ TACTIC:Assert ⌜∀x:ℤ. ((1 * x) = x ∈ ℤ)⌝⋅ }

1
.....assertion..... 
∀x:ℤ. ((1 * x) = x ∈ ℤ)

2
1. ∀x:ℤ. ((1 * x) = x ∈ ℤ)
⊢ ∀[x:ℤ]. (1 * x ~ x)

---

Latex:

---

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


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x:\mBbbZ{}.  ((1  *  x)  =  x)\mkleeneclose{}\mcdot{}

---

Home Index