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 holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
let TD be 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 f be HK-integrable Function of I,REAL; for r being Real holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
let r be Real; 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;
( 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))
;
(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;
verum
end;
hence
tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
by FINSEQ_2:9, Z1; verum