---

Step * of Lemma eq-finite-seqs-implies-eq-upto

∀a,b:ℕ ⟶ ℕ. ∀x:ℕ.  ((↑eq-finite-seqs(a;b;x)) ⇒ (a = b ∈ (ℕx ⟶ ℕ)))
BY
{ ((UnivCD THENA Auto) THEN NatInd (-2) THEN (UnivCD THENA Auto)) }

1
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. ↑eq-finite-seqs(a;b;0)
⊢ a = b ∈ (ℕ0 ⟶ ℕ)

2
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. 0 < x
5. (↑eq-finite-seqs(a;b;x - 1)) ⇒ (a = b ∈ (ℕx - 1 ⟶ ℕ))
6. ↑eq-finite-seqs(a;b;x)
⊢ a = b ∈ (ℕx ⟶ ℕ)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x:\mBbbN{}.    ((\muparrow{}eq-finite-seqs(a;b;x))  {}\mRightarrow{}  (a  =  b))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  NatInd  (-2)  THEN  (UnivCD  THENA  Auto))

---

Home Index