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 = (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']))
let f, g, h be Function of REAL,REAL; :: thesis: ( a <= b & b <= c & f is continuous & g is continuous & h = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b implies integral (((id REAL) (#) h),['a,c']) = (integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c'])) )
assume that
A1: ( a <= b & b <= c ) and
A2: ( f is continuous & g is continuous ) and
A3: h = (f | [.a,b.]) +* (g | [.b,c.]) and
A4: f . b = g . b ; :: thesis: integral (((id REAL) (#) h),['a,c']) = (integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c']))
A55: ( dom f = REAL & dom g = REAL ) by FUNCT_2:def 1;
set A = ['a,c'];
reconsider ff = f as PartFunc of REAL,REAL ;
reconsider gg = g as PartFunc of REAL,REAL ;
A2a: ( ff | ['a,c'] is continuous & gg | ['a,c'] is continuous ) by A2;
( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & g is_integrable_on ['a,c'] & g | ['a,c'] is bounded ) by INTEGRA5:11, INTEGRA5:10, A2a, A55;
then B12: ( (id REAL) (#) f is_integrable_on ['a,c'] & ((id REAL) (#) f) | ['a,c'] is bounded & (id REAL) (#) g is_integrable_on ['a,c'] & ((id REAL) (#) g) | ['a,c'] is bounded ) by Lm3;
set G = (((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.]);
B3a: dom ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) = (dom (((id REAL) (#) f) | [.a,b.])) \/ (dom (((id REAL) (#) g) | [.b,c.])) by FUNCT_4:def 1
.= [.a,b.] \/ (dom (((id REAL) (#) g) | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] by FUNCT_2:def 1
.= [.a,c.] by XXREAL_1:165, A1 ;
AC: ( REAL /\ [.a,c.] c= [.a,c.] & [.a,c.] c= REAL /\ [.a,c.] ) by XBOOLE_0:def 4;
B3b: [.a,c.] = REAL /\ [.a,c.] by AC, XBOOLE_0:def 10
.= (dom ((id REAL) (#) h)) /\ [.a,c.] by FUNCT_2:def 1 ;
for x being object st x in dom ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) holds
((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) h) . x

proof

let x be object ; :: thesis: ( x in dom ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) implies ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) h) . x )
assume Gx: x in dom ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) ; :: thesis: ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) h) . x
then reconsider x = x as Real by B3a;
C1: ( a <= x & x <= c ) by XXREAL_1:1, Gx, B3a;

per cases ( b <= x or x < b ) ;

suppose b <= x ; :: thesis: ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) h) . x

then CC: x in [.b,c.] by C1;
then CC1: x in dom (((id REAL) (#) g) | [.b,c.]) by FUNCT_2:def 1;
CC2: x in dom (g | [.b,c.]) by CC, FUNCT_2:def 1;
((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = (((id REAL) (#) g) | [.b,c.]) . x by FUNCT_4:13, CC1
.= ((id REAL) (#) g) . x by FUNCT_1:49, CC
.= ((id REAL) . x) * (g . x) by VALUED_1:5
.= ((id REAL) . x) * ((g | [.b,c.]) . x) by FUNCT_1:49, CC
.= ((id REAL) . x) * (((f | [.a,b.]) +* (g | [.b,c.])) . x) by CC2, FUNCT_4:13
.= ((id REAL) (#) h) . x by A3, VALUED_1:5 ;
hence ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) h) . x ; :: thesis: verum

end;

suppose DX: x < b ; :: thesis: ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) h) . x

then CCa: x in [.a,b.] by C1;
DD1: not x in dom (((id REAL) (#) g) | [.b,c.]) by XXREAL_1:1, DX;
DD2: not x in dom (g | [.b,c.]) by XXREAL_1:1, DX;
((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = (((id REAL) (#) f) | [.a,b.]) . x by FUNCT_4:11, DD1
.= ((id REAL) (#) f) . x by FUNCT_1:49, CCa
.= ((id REAL) . x) * (f . x) by VALUED_1:5
.= ((id REAL) . x) * ((f | [.a,b.]) . x) by FUNCT_1:49, CCa
.= ((id REAL) . x) * (((f | [.a,b.]) +* (g | [.b,c.])) . x) by DD2, FUNCT_4:11
.= ((id REAL) (#) h) . x by A3, VALUED_1:5 ;
hence ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) h) . x ; :: thesis: verum

end;

end;

end;

then B3: ((id REAL) (#) h) | [.a,c.] = (((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.]) by FUNCT_1:46, B3a, B3b;
B4: ((id REAL) (#) f) . b = ((id REAL) . b) * (g . b) by A4, VALUED_1:5
.= ((id REAL) (#) g) . b by VALUED_1:5 ;
h is continuous by Th24, A1, A2, A3, A4;
then (id REAL) (#) h is_integrable_on ['a,c'] by integra51011;
hence integral (((id REAL) (#) h),['a,c']) = (integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c'])) by Th18Z, A1, B12, B3, B4; :: thesis: verum