---

Step * 1 of Lemma mul-initial-seg-step

.....basecase..... 
1. f : ℕ ⟶ ℕ
2. m : ℕ+
⊢ (mul-initial-seg(f) 1) = ((mul-initial-seg(f) (1 - 1)) * (f (1 - 1))) ∈ ℤ
BY
{ (RepUR ``mul-initial-seg upto`` 0 THEN RepeatFor 2 ((RecUnfold `from-upto` 0 THEN Reduce 0)) THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  (mul-initial-seg(f)  1)  =  ((mul-initial-seg(f)  (1  -  1))  *  (f  (1  -  1)))


By

---

Latex:
(RepUR  ``mul-initial-seg  upto``  0
  THEN  RepeatFor  2  ((RecUnfold  `from-upto`  0  THEN  Reduce  0))
  THEN  Auto)

---

Home Index