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