theorem :: FUZZY_6:8

for a, b, c being Real
for f being Function of REAL,REAL st a < b & b <= c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & ( for x being Real st x in ['b,c'] holds
f . x = 0 ) holds
centroid (f,['a,c']) = centroid (f,['a,b'])