let A be non empty closed_interval Subset of REAL; 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 A
let a be 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 A
let f, g, h be Function of REAL,REAL; ( 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 A )
assume A1:
( f | A is bounded & f is_integrable_on A )
; ( not g | A is bounded or not g is_integrable_on A or not a in A or not h = (f | ].-infty,a.]) +* (g | [.a,+infty.[) or not f . a = g . a or h is_integrable_on A )
assume A2:
( g | A is bounded & g is_integrable_on A )
; ( not a in A or not h = (f | ].-infty,a.]) +* (g | [.a,+infty.[) or not f . a = g . a or h is_integrable_on A )
assume A3:
a in A
; ( not h = (f | ].-infty,a.]) +* (g | [.a,+infty.[) or not f . a = g . a or h is_integrable_on A )
assume A4:
h = (f | ].-infty,a.]) +* (g | [.a,+infty.[)
; ( not f . a = g . a or h is_integrable_on A )
assume A40:
f . a = g . a
; h is_integrable_on 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;
B2s:
dom h = REAL
by FUNCT_2:def 1;
B21a:
dom f = REAL
by FUNCT_2:def 1;
B22a:
dom g = REAL
by FUNCT_2:def 1;
( [.(lower_bound A),a.] c= [.(lower_bound A),(upper_bound A).] & [.a,(upper_bound A).] c= [.(lower_bound A),(upper_bound A).] )
by XXREAL_1:34, B1;
then
( [.(lower_bound A),a.] c= A & [.a,(upper_bound A).] c= A )
by INTEGRA1:4;
then B301:
( ['(lower_bound A),a'] c= A & ['a,(upper_bound A)'] c= A )
by INTEGRA5:def 3, B1;
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 ;
( 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'])
;
(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 ;
( 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.[))
;
(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
;
(f | ].-infty,a.]) . x =
(f | ].-infty,a.]) . a
by TARSKI:def 1, T1, T2
.=
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;
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;
verum
end;
then B5:
f | ['(lower_bound A),a'] = h | ['(lower_bound A),a']
by FUNCT_1:2, B51;
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 ;
( 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)'])
;
(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;
verum
end;
then
g | ['a,(upper_bound A)'] = h | ['a,(upper_bound A)']
by FUNCT_1:2, B61;
then B3:
( h | ['(lower_bound A),a'] is bounded & h | ['a,(upper_bound A)'] is bounded )
by B5, B301, RFUNCT_1:74, A1, A2;
B77:
f is_integrable_on ['(lower_bound A),a']
by B11, INTEGRA617, B21a, A5, A1, A3;
g is_integrable_on ['a,(upper_bound A)']
by B11, INTEGRA617, B22a, A5, A2, A3;
then
( 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;
hence
h is_integrable_on A
by B1, B2s, B3, INTEGR241, A5; verum