---

Step * 1 of Lemma rsum_product


1. a : ℤ
2. b : ℤ
3. c : ℤ
4. d : ℤ
5. x : {a..b + 1-} ⟶ ℝ
6. y : {c..d + 1-} ⟶ ℝ
⊢ (Σ{y[j] | c≤j≤d} * Σ{x[i] | a≤i≤b}) = Σ{Σ{x[i] * y[j] | c≤j≤d} | a≤i≤b}
BY
{ ((RWO "rsum_linearity2<" 0 THEN Auto)⋅ THEN BLemma `rsum_functionality` THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
4.  d  :  \mBbbZ{}
5.  x  :  \{a..b  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
6.  y  :  \{c..d  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
\mvdash{}  (\mSigma{}\{y[j]  |  c\mleq{}j\mleq{}d\}  *  \mSigma{}\{x[i]  |  a\mleq{}i\mleq{}b\})  =  \mSigma{}\{\mSigma{}\{x[i]  *  y[j]  |  c\mleq{}j\mleq{}d\}  |  a\mleq{}i\mleq{}b\}


By

---

Latex:
((RWO  "rsum\_linearity2<"  0  THEN  Auto)\mcdot{}
  THEN  BLemma  `rsum\_functionality`
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index