ι : Type u_2
inst✝² : Fintype ι
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ ↑(Measure.toBoxAdditive volume) I • x = (∏ j : ι, (upper I j - lower I j)) • x
ι : Type u_2
inst✝² : Fintype ι
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ ↑(↑BoxAdditiveMap.volume I) x = (∏ j : ι, (upper I j - lower I j)) • x
rw [BoxAdditiveMap.volume, toSMul_apply]