for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b <= c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] holds
( f is_integrable_on ['a,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )