let a, b, c be Real; :: thesis: for f, g, h being Function of REAL,REAL st a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & 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 continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & 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 continuous & g is continuous ) and
A3: h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) and
A4: f . b = g . b ; :: thesis: integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))
B1: ( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded ) by FUZZY_6:25, A2;
B2: ( g is_integrable_on ['a,c'] & g | ['a,c'] is bounded ) by FUZZY_6:25, A2;
reconsider hh = h as PartFunc of REAL,REAL ;
D1p: REAL = dom h by FUNCT_2:def 1;
then hh | [.a,c.] is continuous by FUZZY_7:41, A1, A2, A4, A3;
then hh | ['a,c'] is continuous by XXREAL_0:2, A1, INTEGRA5:def 3;
then h is_integrable_on ['a,c'] by INTEGRA5:11, D1p;
hence integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c'])) by FUZZY_6:33, B1, B2, A3, A1, A4; :: thesis: verum