for A being Subset of REAL
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
tagged_sum (f,TD) = 0