let I be non empty closed_interval Subset of REAL; 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; 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; 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; 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; ( 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
; (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; verum