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 holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
let TD be tagged_division of I; :: thesis: for f being HK-integrable Function of I,REAL
for r being Real holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
let f be HK-integrable Function of I,REAL; :: thesis: for r being Real holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
let r be Real; :: thesis: tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
Z1: len (r * (tagged_volume (f,TD))) = len (tagged_volume (f,TD)) by RVSUM_1:117
.= len TD by Def4
.= len (tagged_volume ((r (#) f),TD)) by Def4 ;
for i being Nat st i in dom (tagged_volume ((r (#) f),TD)) holds
(tagged_volume ((r (#) f),TD)) . i = (r * (tagged_volume (f,TD))) . i

proof

let i be Nat; :: thesis: ( i in dom (tagged_volume ((r (#) f),TD)) implies (tagged_volume ((r (#) f),TD)) . i = (r * (tagged_volume (f,TD))) . i )
assume i in dom (tagged_volume ((r (#) f),TD)) ; :: thesis: (tagged_volume ((r (#) f),TD)) . i = (r * (tagged_volume (f,TD))) . i
then i in Seg (len (tagged_volume ((r (#) f),TD))) by FINSEQ_1:def 3;
then i in Seg (len TD) by Def4;
then A1: i in dom TD by FINSEQ_1:def 3;
then (tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i))) by Th31
.= r * ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))))
.= r * ((tagged_volume (f,TD)) . i) by A1, Def4 ;
hence (tagged_volume ((r (#) f),TD)) . i = (r * (tagged_volume (f,TD))) . i by RVSUM_1:45; :: thesis: verum

end;

hence tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD)) by FINSEQ_2:9, Z1; :: thesis: verum