theorem :: FUZZY_7:22

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 holds
( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )