theorem Th17: :: FUZZY_7:24

for A, B being non empty closed_interval Subset of REAL
for f being Function of REAL,REAL st lower_bound B <> upper_bound B & B c= A & f is_integrable_on A & f | A is bounded & ( for x being Real st x in A \ B holds
f . x = 0 ) & f . (lower_bound B) = 0 & f . (upper_bound B) = 0 holds
centroid (f,A) = centroid (f,B)