---

Step * of Lemma add_functionality_wrt_eq

∀[i1,i2,j1,j2:ℤ].  ((i1 + i2) = (j1 + j2) ∈ ℤ) supposing ((i2 = j2 ∈ ℤ) and (i1 = j1 ∈ ℤ))
BY
{ ((UnivCD THENA Auto) THEN EqCD THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  EqCD  THEN  Trivial)

---

Home Index