theorem Th18Z: :: FUZZY_6:33

for a, b, c being Real
for f, g, h being Function of REAL,REAL st a <= b & b <= c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & g is_integrable_on ['a,c'] & g | ['a,c'] is bounded & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & h is_integrable_on ['a,c'] & f . b = g . b holds
integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))