theorem :: FUZZY_7:23

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