---

Step * of Lemma mul-list-bag-product

∀L:ℤ List. (Π(L)  = Π(L) ∈ ℤ)
BY
{ (RepUR ``int-bag-product bag-product bag-summation bag-accum mul-list`` 0 THEN (D 0 THENA Auto)) }

1
1. L : ℤ List
⊢ reduce(λx,y. (x * y);1;L) = accumulate (with value c and list item x): x * cover list:  Lwith starting value: 1) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List.  (\mPi{}(L)    =  \mPi{}(L))


By

---

Latex:
(RepUR  ``int-bag-product  bag-product  bag-summation  bag-accum  mul-list``  0  THEN  (D  0  THENA  Auto))

---

Home Index