theorem Th33: :: COUSIN2:36

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f, g being HK-integrable Function of I,REAL
for i being Nat st i in dom TD holds
(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))))