---

Step * 3 1 2 of Lemma equipollent-multiply


1. a : ℕ
2. b : ℕ
3. a3 : ℕa
4. a4 : ℕb
5. a5 : ℕa
6. a6 : ℕb
7. ((a3 * b) + a4) = ((a5 * b) + a6) ∈ ℕa * b
8. a3 = a5 ∈ ℤ
⊢ <a3, a4> = <a5, a6> ∈ (ℕa × ℕb)
BY
{ (HypSubst' -1 -2 THEN EqCD THEN Auto') }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  a3  :  \mBbbN{}a
4.  a4  :  \mBbbN{}b
5.  a5  :  \mBbbN{}a
6.  a6  :  \mBbbN{}b
7.  ((a3  *  b)  +  a4)  =  ((a5  *  b)  +  a6)
8.  a3  =  a5
\mvdash{}  <a3,  a4>  =  <a5,  a6>


By

---

Latex:
(HypSubst'  -1  -2  THEN  EqCD  THEN  Auto')

---

Home Index