let I be non empty closed_interval Subset of REAL; :: thesis: for TD being tagged_division of I
for f being HK-integrable Function of I,REAL
for r being Real
for i being Nat st i in dom TD holds
(tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))
let TD be tagged_division of I; :: thesis: for f being HK-integrable Function of I,REAL
for r being Real
for i being Nat st i in dom TD holds
(tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))
let f be HK-integrable Function of I,REAL; :: thesis: for r being Real
for i being Nat st i in dom TD holds
(tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))
let r be Real; :: thesis: for i being Nat st i in dom TD holds
(tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))
let i be Nat; :: thesis: ( i in dom TD implies (tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i))) )
assume i in dom TD ; :: thesis: (tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))
then (tagged_volume ((r (#) f),TD)) . i = ((r (#) f) . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) by Def4;
hence (tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i))) by VALUED_1:6; :: thesis: verum