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
( h is_integrable_on ['(lower_bound A),a'] & h is_integrable_on ['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
( h is_integrable_on ['(lower_bound A),a'] & h is_integrable_on ['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 ( h is_integrable_on ['(lower_bound A),a'] & h is_integrable_on ['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: ( h is_integrable_on ['(lower_bound A),a'] & h is_integrable_on ['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 ;
a in [.(lower_bound A),(upper_bound A).] by INTEGRA5:def 3, SEQ_4:11, A3, A5;
then B1: ( lower_bound A <= a & a <= upper_bound A ) by XXREAL_1:1;
B11: lower_bound A <= upper_bound A by SEQ_4:11;
B21a: dom f = REAL by FUNCT_2:def 1;
B22a: dom g = REAL by FUNCT_2:def 1;
B51: dom (f | ['(lower_bound A),a']) = ['(lower_bound A),a'] by FUNCT_2:def 1
.= dom (h | ['(lower_bound A),a']) by FUNCT_2:def 1 ;
B5g: for x being object st x in dom (f | ['(lower_bound A),a']) holds
(f | ['(lower_bound A),a']) . x = (h | ['(lower_bound A),a']) . x

proof

let x be object ; :: thesis: ( x in dom (f | ['(lower_bound A),a']) implies (f | ['(lower_bound A),a']) . x = (h | ['(lower_bound A),a']) . x )
assume D1: x in dom (f | ['(lower_bound A),a']) ; :: thesis: (f | ['(lower_bound A),a']) . x = (h | ['(lower_bound A),a']) . x
then x in ['(lower_bound A),a'] ;
then reconsider x = x as Element of REAL ;
D1f: dom (f | ['(lower_bound A),a']) = ['(lower_bound A),a'] by FUNCT_2:def 1
.= [.(lower_bound A),a.] by INTEGRA5:def 3, B1 ;
then D7: ( lower_bound A <= x & x <= a ) by XXREAL_1:1, D1;
D3u: for x being object st x in (dom (f | ].-infty,a.])) /\ (dom (g | [.a,+infty.[)) holds
(f | ].-infty,a.]) . x = (g | [.a,+infty.[) . x

proof

let x be object ; :: thesis: ( x in (dom (f | ].-infty,a.])) /\ (dom (g | [.a,+infty.[)) implies (f | ].-infty,a.]) . x = (g | [.a,+infty.[) . x )
assume T1: x in (dom (f | ].-infty,a.])) /\ (dom (g | [.a,+infty.[)) ; :: thesis: (f | ].-infty,a.]) . x = (g | [.a,+infty.[) . x
T2: (dom (f | ].-infty,a.])) /\ (dom (g | [.a,+infty.[)) = ].-infty,a.] /\ (dom (g | [.a,+infty.[)) by FUNCT_2:def 1
.= ].-infty,a.] /\ [.a,+infty.[ by FUNCT_2:def 1
.= [.a,a.] by XXREAL_1:272
.= {a} by XXREAL_1:17 ;
then (f | ].-infty,a.]) . x = (f | ].-infty,a.]) . a by TARSKI:def 1, T1
.= f . a by FUNCT_1:49, XXREAL_1:234
.= (g | [.a,+infty.[) . a by FUNCT_1:49, XXREAL_1:236, A40 ;
hence (f | ].-infty,a.]) . x = (g | [.a,+infty.[) . x by TARSKI:def 1, T1, T2; :: thesis: verum

end;

x in ].-infty,a.] by XXREAL_1:234, D7;
then D4: x in dom (f | ].-infty,a.]) by FUNCT_2:def 1;
(f | ['(lower_bound A),a']) . x = f . x by FUNCT_1:49, D1
.= (f | ].-infty,a.]) . x by FUNCT_1:49, XXREAL_1:234, D7
.= ((f | ].-infty,a.]) +* (g | [.a,+infty.[)) . x by D4, FUNCT_4:15, D3u, PARTFUN1:def 4
.= (h | [.(lower_bound A),a.]) . x by FUNCT_1:49, A4, D1f, D1 ;
hence (f | ['(lower_bound A),a']) . x = (h | ['(lower_bound A),a']) . x by INTEGRA5:def 3, B1; :: thesis: verum

end;

B61: dom (g | ['a,(upper_bound A)']) = ['a,(upper_bound A)'] by FUNCT_2:def 1
.= dom (h | ['a,(upper_bound A)']) by FUNCT_2:def 1 ;
B6f: for x being object st x in dom (g | ['a,(upper_bound A)']) holds
(g | ['a,(upper_bound A)']) . x = (h | ['a,(upper_bound A)']) . x

proof

let x be object ; :: thesis: ( x in dom (g | ['a,(upper_bound A)']) implies (g | ['a,(upper_bound A)']) . x = (h | ['a,(upper_bound A)']) . x )
assume E1: x in dom (g | ['a,(upper_bound A)']) ; :: thesis: (g | ['a,(upper_bound A)']) . x = (h | ['a,(upper_bound A)']) . x
then x in ['a,(upper_bound A)'] ;
then reconsider x = x as Element of REAL ;
E2x: dom (g | ['a,(upper_bound A)']) = ['a,(upper_bound A)'] by FUNCT_2:def 1
.= [.a,(upper_bound A).] by INTEGRA5:def 3, B1 ;
then E3x: a <= x by XXREAL_1:1, E1;
then x in [.a,+infty.[ by XXREAL_1:236;
then E4: x in dom (g | [.a,+infty.[) by FUNCT_2:def 1;
(g | ['a,(upper_bound A)']) . x = g . x by FUNCT_1:49, E1
.= (g | [.a,+infty.[) . x by FUNCT_1:49, E3x, XXREAL_1:236
.= h . x by A4, FUNCT_4:13, E4
.= (h | [.a,(upper_bound A).]) . x by FUNCT_1:49, E2x, E1 ;
hence (g | ['a,(upper_bound A)']) . x = (h | ['a,(upper_bound A)']) . x by INTEGRA5:def 3, B1; :: thesis: verum

end;

B77: f is_integrable_on ['(lower_bound A),a'] by B11, FUZZY_8:13, B21a, A5, A1, A3;
g is_integrable_on ['a,(upper_bound A)'] by B11, FUZZY_8:13, B22a, A5, A2, A3;
hence ( h is_integrable_on ['(lower_bound A),a'] & h is_integrable_on ['a,(upper_bound A)'] ) by B77, B6f, FUNCT_1:2, B61, B5g, B51; :: thesis: verum