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 holds tagged_volume ((f + g),TD) = (tagged_volume (f,TD)) + (tagged_volume (g,TD))