let a, b, c be Real; :: thesis: 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 = (f | ].-infty,b.]) +* (g | [.b,+infty.[) & f . b = g . b holds
integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))
let f, g, h be Function of REAL,REAL; :: thesis: ( 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 = (f | ].-infty,b.]) +* (g | [.b,+infty.[) & f . b = g . b implies integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c'])) )
assume that
A1: ( a <= b & b <= c ) and
A2: ( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & g is_integrable_on ['a,c'] & g | ['a,c'] is bounded ) and
A3: h = (f | ].-infty,b.]) +* (g | [.b,+infty.[) and
A4: f . b = g . b ; :: thesis: integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))
A5: h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) by A1, FUZZY711, A3;
b in [.a,c.] by A1;
then b in ['a,c'] by INTEGRA5:def 3, XXREAL_0:2, A1;
then h is_integrable_on ['a,c'] by Th39, A2, A3, A4;
hence integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c'])) by FUZZY_6:33, A1, A2, A4, A5; :: thesis: verum