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 (((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 | [.a,c.] = (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 | [.a,c.] = (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']))
A5g: ( dom f = REAL & dom g = REAL ) by FUNCT_2:def 1;
set A = ['a,c'];
reconsider ff = f, 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, A5g, A2a;
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 FUZZY_6:6;
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 ;
XX: [.a,c.] c= REAL /\ [.a,c.] by XBOOLE_0:def 4;
AC: [.a,c.] = REAL /\ [.a,c.]

proof

REAL /\ [.a,c.] c= [.a,c.] by XBOOLE_0:def 4;
hence [.a,c.] = REAL /\ [.a,c.] by XX, XBOOLE_0:def 10; :: thesis: verum

end;

H1: dom ((id REAL) (#) (h | [.a,c.])) = (dom (id REAL)) /\ (dom (h | [.a,c.])) by VALUED_1:def 4
.= [.a,c.] by AC, FUNCT_2:def 1 ;
H2: dom (((id REAL) (#) h) | [.a,c.]) = [.a,c.] by FUNCT_2:def 1;
H33: for x being object st x in dom (((id REAL) (#) h) | [.a,c.]) holds
((id REAL) (#) (h | [.a,c.])) . x = (((id REAL) (#) h) | [.a,c.]) . x

proof

let x be object ; :: thesis: ( x in dom (((id REAL) (#) h) | [.a,c.]) implies ((id REAL) (#) (h | [.a,c.])) . x = (((id REAL) (#) h) | [.a,c.]) . x )
assume H4: x in dom (((id REAL) (#) h) | [.a,c.]) ; :: thesis: ((id REAL) (#) (h | [.a,c.])) . x = (((id REAL) (#) h) | [.a,c.]) . x
then reconsider x = x as Real ;
((id REAL) (#) (h | [.a,c.])) . x = ((id REAL) . x) * ((h | [.a,c.]) . x) by VALUED_1:5
.= ((id REAL) . x) * (h . x) by FUNCT_1:49, H4
.= ((id REAL) (#) h) . x by VALUED_1:5
.= (((id REAL) (#) h) | [.a,c.]) . x by FUNCT_1:49, H4 ;
hence ((id REAL) (#) (h | [.a,c.])) . x = (((id REAL) (#) h) | [.a,c.]) . x ; :: thesis: verum

end;

B3b: [.a,c.] = (dom ((id REAL) (#) (h | [.a,c.]))) /\ [.a,c.] by H1;
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 | [.a,c.])) . 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 | [.a,c.])) . x )
assume Xac: 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 | [.a,c.])) . x
then reconsider x = x as Real by B3a;
C1: ( a <= x & x <= c ) by Xac, B3a, XXREAL_1:1;

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 | [.a,c.])) . 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 | [.a,c.])) . x by A3, VALUED_1:5 ;
hence ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) (h | [.a,c.])) . x ; :: thesis: verum

end;

suppose DX: x < b ; :: thesis: ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) (h | [.a,c.])) . 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 | [.a,c.])) . x by A3, VALUED_1:5 ;
hence ((((id REAL) (#) f) | [.a,b.]) +* (((id REAL) (#) g) | [.b,c.])) . x = ((id REAL) (#) (h | [.a,c.])) . x ; :: thesis: verum

end;

end;

end;

then B3z: ((id REAL) (#) (h | [.a,c.])) | [.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 ;
reconsider hh = h as PartFunc of REAL,REAL ;
D1p: REAL = dom h by FUNCT_2:def 1;
then hh | [.a,c.] is continuous by Lm22b1p, 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'] & h | ['a,c'] is bounded ) by INTEGRA5:10, INTEGRA5:11, D1p;
then (id REAL) (#) h is_integrable_on ['a,c'] by FUZZY_6:6;
hence integral (((id REAL) (#) h),['a,c']) = (integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c'])) by FUZZY_6:33, A1, B12, B4, FUNCT_1:2, H1, H2, H33, B3z; :: thesis: verum