let I be non empty closed_interval Subset of REAL; :: thesis: for TD being tagged_division of I
for f, g being HK-integrable Function of I,REAL holds tagged_volume ((f + g),TD) = (tagged_volume (f,TD)) + (tagged_volume (g,TD))
let TD be tagged_division of I; :: thesis: for f, g being HK-integrable Function of I,REAL holds tagged_volume ((f + g),TD) = (tagged_volume (f,TD)) + (tagged_volume (g,TD))
let f, g be HK-integrable Function of I,REAL; :: thesis: tagged_volume ((f + g),TD) = (tagged_volume (f,TD)) + (tagged_volume (g,TD))
( len (tagged_volume (f,TD)) = len TD & len (tagged_volume (g,TD)) = len TD ) by Def4;
then reconsider R1 = tagged_volume (f,TD), R2 = tagged_volume (g,TD) as Element of (len TD) -tuples_on REAL by FINSEQ_2:92;
len (tagged_volume (f,TD)) = len TD by Def4
.= len (tagged_volume (g,TD)) by Def4 ;
then Z1: len ((tagged_volume (f,TD)) + (tagged_volume (g,TD))) = len (tagged_volume (f,TD)) by RVSUM_1:115
.= len TD by Def4
.= len (tagged_volume ((f + g),TD)) by Def4 ;
for i being Nat st i in dom (tagged_volume ((f + g),TD)) holds
(tagged_volume ((f + g),TD)) . i = ((tagged_volume (f,TD)) + (tagged_volume (g,TD))) . i

proof

let i be Nat; :: thesis: ( i in dom (tagged_volume ((f + g),TD)) implies (tagged_volume ((f + g),TD)) . i = ((tagged_volume (f,TD)) + (tagged_volume (g,TD))) . i )
assume i in dom (tagged_volume ((f + g),TD)) ; :: thesis: (tagged_volume ((f + g),TD)) . i = ((tagged_volume (f,TD)) + (tagged_volume (g,TD))) . i
then i in Seg (len (tagged_volume ((f + g),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 ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) by Th33
.= ((tagged_volume (f,TD)) . i) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) by A1, Def4
.= (R1 . i) + (R2 . i) by A1, Def4
.= ((tagged_volume (f,TD)) + (tagged_volume (g,TD))) . i by RVSUM_1:11 ;
hence (tagged_volume ((f + g),TD)) . i = ((tagged_volume (f,TD)) + (tagged_volume (g,TD))) . i ; :: thesis: verum

end;

hence tagged_volume ((f + g),TD) = (tagged_volume (f,TD)) + (tagged_volume (g,TD)) by FINSEQ_2:9, Z1; :: thesis: verum