---

Step * of Lemma mul_functionality_wrt_eq

∀[i1,i2,j1,j2:ℤ].  ((i1 * i2) = (j1 * j2) ∈ ℤ) supposing ((i2 = j2 ∈ ℤ) and (i1 = j1 ∈ ℤ))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[i1,i2,j1,j2:\mBbbZ{}].    ((i1  *  i2)  =  (j1  *  j2))  supposing  ((i2  =  j2)  and  (i1  =  j1))


By

---

Latex:
Auto

---

Home Index