theorem :: FUZZY_9:36

for A being non empty closed_interval Subset of REAL
for a being Real
for f, g, h being Function of REAL,REAL st f | A is bounded & f is_integrable_on A & g | A is bounded & g is_integrable_on A & a in A & h = (f | ].-infty,a.]) +* (g | [.a,+infty.[) & f . a = g . a holds
integral (h,A) = (integral (f,['(lower_bound A),a'])) + (integral (g,['a,(upper_bound A)']))