let A be non empty closed_interval Subset of REAL; :: thesis: 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)']))
let a be Real; :: thesis: 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)']))
let f, g, h be Function of REAL,REAL; :: thesis: ( 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 implies integral (h,A) = (integral (f,['(lower_bound A),a'])) + (integral (g,['a,(upper_bound A)'])) )
assume that
A1: ( f | A is bounded & f is_integrable_on A ) and
A2: ( g | A is bounded & g is_integrable_on A ) and
A3: a in A and
A4: h = (f | ].-infty,a.]) +* (g | [.a,+infty.[) and
A40: f . a = g . a ; :: thesis: integral (h,A) = (integral (f,['(lower_bound A),a'])) + (integral (g,['a,(upper_bound A)']))
set AA = ['(lower_bound A),(upper_bound A)'];
A5: ['(lower_bound A),(upper_bound A)'] = [.(lower_bound A),(upper_bound A).] by INTEGRA5:def 3, SEQ_4:11
.= A by INTEGRA1:4 ;
then a in [.(lower_bound A),(upper_bound A).] by INTEGRA5:def 3, SEQ_4:11, A3;
then ( lower_bound A <= a & a <= upper_bound A ) by XXREAL_1:1;
hence integral (h,A) = (integral (f,['(lower_bound A),a'])) + (integral (g,['a,(upper_bound A)'])) by A40, A4, FUZZY_8:16, A2, A1, A5; :: thesis: verum