let a, b, c be Real; for f, g, h being Function of REAL,REAL st a <= b & b <= c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & g is_integrable_on ['a,c'] & g | ['a,c'] is bounded & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & h is_integrable_on ['a,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; ( a <= b & b <= c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & g is_integrable_on ['a,c'] & g | ['a,c'] is bounded & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & h is_integrable_on ['a,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_integrable_on ['a,c'] & f | ['a,c'] is bounded )
and
A3:
( g is_integrable_on ['a,c'] & g | ['a,c'] is bounded )
and
A4:
h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.])
and
A0:
h is_integrable_on ['a,c']
and
A5:
f . b = g . b
; integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))
B10:
f | [.a,b.] tolerates g | [.b,c.]
proof
for
x being
object st
x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) holds
(f | [.a,b.]) . x = (g | [.b,c.]) . x
proof
let x be
object ;
( x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) implies (f | [.a,b.]) . x = (g | [.b,c.]) . x )
assume T1:
x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.]))
;
(f | [.a,b.]) . x = (g | [.b,c.]) . x
T2:
(dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) =
[.a,b.] /\ (dom (g | [.b,c.]))
by FUNCT_2:def 1
.=
[.a,b.] /\ [.b,c.]
by FUNCT_2:def 1
.=
{b}
by XXREAL_1:418, A1
;
(f | [.a,b.]) . x =
(f | [.a,b.]) . b
by TARSKI:def 1, T1, T2
.=
f . b
by FUNCT_1:49, XXREAL_1:1, A1
.=
(g | [.b,c.]) . b
by FUNCT_1:49, XXREAL_1:1, A1, A5
;
hence
(f | [.a,b.]) . x = (g | [.b,c.]) . x
by TARSKI:def 1, T1, T2;
verum
end;
hence
f | [.a,b.] tolerates g | [.b,c.]
by PARTFUN1:def 4;
verum
end;
reconsider h1 = h | ['a,b'] as PartFunc of ['a,b'],REAL ;
reconsider f1 = f | ['a,b'] as PartFunc of ['a,b'],REAL ;
reconsider H = upper_sum_set h1 as Function of (divs ['a,b']),REAL ;
reconsider F = upper_sum_set f1 as Function of (divs ['a,b']),REAL ;
A6:
H = F
proof
for
D being
object st
D in divs ['a,b'] holds
H . D = F . D
proof
let D be
object ;
( D in divs ['a,b'] implies H . D = F . D )
assume
D in divs ['a,b']
;
H . D = F . D
then reconsider D =
D as
Division of
['a,b'] by INTEGRA1:def 3;
set uvh1 =
upper_volume (
h1,
D);
set uvf1 =
upper_volume (
f1,
D);
(
len D = len (upper_volume (h1,D)) &
len D = len (upper_volume (f1,D)) )
by INTEGRA1:def 6;
then A8:
dom (upper_volume (h1,D)) = dom (upper_volume (f1,D))
by FINSEQ_3:29;
B4:
upper_volume (
h1,
D)
= upper_volume (
f1,
D)
proof
for
i being
Element of
NAT st
i in dom (upper_volume (h1,D)) holds
(upper_volume (h1,D)) . i = (upper_volume (f1,D)) . i
proof
let i be
Element of
NAT ;
( i in dom (upper_volume (h1,D)) implies (upper_volume (h1,D)) . i = (upper_volume (f1,D)) . i )
assume B1:
i in dom (upper_volume (h1,D))
;
(upper_volume (h1,D)) . i = (upper_volume (f1,D)) . i
len D = len (upper_volume (h1,D))
by INTEGRA1:def 6;
then B2:
i in dom D
by FINSEQ_3:29, B1;
B5:
divset (
D,
i)
c= ['a,b']
by INTEGRA1:8, B2;
B7:
h | (divset (D,i)) = f | (divset (D,i))
proof
for
x being
object st
x in divset (
D,
i) holds
(h | (divset (D,i))) . x = (f | (divset (D,i))) . x
proof
let x be
object ;
( x in divset (D,i) implies (h | (divset (D,i))) . x = (f | (divset (D,i))) . x )
assume B8:
x in divset (
D,
i)
;
(h | (divset (D,i))) . x = (f | (divset (D,i))) . x
then B9X:
x in ['a,b']
by B5;
then B9:
x in [.a,b.]
by INTEGRA5:def 3, A1;
reconsider x =
x as
Real by B8;
(
a <= x &
x <= b )
by XXREAL_1:1, B9;
then B9c:
(
a <= x &
x <= c )
by XXREAL_0:2, A1;
dom (f | [.a,b.]) = [.a,b.]
by FUNCT_2:def 1;
then B11:
x in dom (f | [.a,b.])
by B9X, INTEGRA5:def 3, A1;
(h | (divset (D,i))) . x =
h . x
by B8, FUNCT_1:49
.=
(h | [.a,c.]) . x
by FUNCT_1:49, B9c, XXREAL_1:1
.=
(f | [.a,b.]) . x
by B10, FUNCT_4:15, B11, A4
.=
f . x
by B9, FUNCT_1:49
;
hence
(h | (divset (D,i))) . x = (f | (divset (D,i))) . x
by B8, FUNCT_1:49;
verum
end;
hence
h | (divset (D,i)) = f | (divset (D,i))
by FUNCT_2:12;
verum
end;
B3:
h1 | (divset (D,i)) =
h | (divset (D,i))
by B5, FUNCT_1:51
.=
f1 | (divset (D,i))
by B5, FUNCT_1:51, B7
;
(upper_volume (h1,D)) . i = (upper_bound (rng (f1 | (divset (D,i))))) * (vol (divset (D,i)))
by B3, INTEGRA1:def 6, B2;
hence
(upper_volume (h1,D)) . i = (upper_volume (f1,D)) . i
by INTEGRA1:def 6, B2;
verum
end;
hence
upper_volume (
h1,
D)
= upper_volume (
f1,
D)
by PARTFUN1:5, A8;
verum
end;
H . D =
upper_sum (
h1,
D)
by INTEGRA1:def 10
.=
Sum (upper_volume (f1,D))
by B4, INTEGRA1:def 8
.=
upper_sum (
f1,
D)
by INTEGRA1:def 8
.=
F . D
by INTEGRA1:def 10
;
hence
H . D = F . D
;
verum
end;
hence
H = F
by FUNCT_2:12;
verum
end;
B6: integral (h,['a,b']) =
integral h1
by INTEGRA5:def 2
.=
upper_integral h1
by INTEGRA1:def 17
.=
lower_bound (rng (upper_sum_set f1))
by A6, INTEGRA1:def 14
.=
upper_integral f1
by INTEGRA1:def 14
.=
integral f1
by INTEGRA1:def 17
.=
integral (f,['a,b'])
by INTEGRA5:def 2
;
reconsider h2 = h | ['b,c'] as PartFunc of ['b,c'],REAL ;
reconsider g1 = g | ['b,c'] as PartFunc of ['b,c'],REAL ;
reconsider H1 = upper_sum_set h2 as Function of (divs ['b,c']),REAL ;
reconsider G = upper_sum_set g1 as Function of (divs ['b,c']),REAL ;
A66:
H1 = G
proof
for
D being
object st
D in divs ['b,c'] holds
H1 . D = G . D
proof
let D be
object ;
( D in divs ['b,c'] implies H1 . D = G . D )
assume
D in divs ['b,c']
;
H1 . D = G . D
then reconsider D =
D as
Division of
['b,c'] by INTEGRA1:def 3;
set uvh2 =
upper_volume (
h2,
D);
set uvg1 =
upper_volume (
g1,
D);
(
len D = len (upper_volume (h2,D)) &
len D = len (upper_volume (g1,D)) )
by INTEGRA1:def 6;
then A8:
dom (upper_volume (h2,D)) = dom (upper_volume (g1,D))
by FINSEQ_3:29;
B4:
upper_volume (
h2,
D)
= upper_volume (
g1,
D)
proof
for
i being
Element of
NAT st
i in dom (upper_volume (h2,D)) holds
(upper_volume (h2,D)) . i = (upper_volume (g1,D)) . i
proof
let i be
Element of
NAT ;
( i in dom (upper_volume (h2,D)) implies (upper_volume (h2,D)) . i = (upper_volume (g1,D)) . i )
assume B1:
i in dom (upper_volume (h2,D))
;
(upper_volume (h2,D)) . i = (upper_volume (g1,D)) . i
reconsider i =
i as
Nat ;
len D = len (upper_volume (h2,D))
by INTEGRA1:def 6;
then B2:
i in dom D
by FINSEQ_3:29, B1;
B5:
divset (
D,
i)
c= ['b,c']
by INTEGRA1:8, B2;
B7:
h | (divset (D,i)) = g | (divset (D,i))
proof
for
x being
object st
x in divset (
D,
i) holds
(h | (divset (D,i))) . x = (g | (divset (D,i))) . x
proof
let x be
object ;
( x in divset (D,i) implies (h | (divset (D,i))) . x = (g | (divset (D,i))) . x )
assume B8:
x in divset (
D,
i)
;
(h | (divset (D,i))) . x = (g | (divset (D,i))) . x
then B9X:
x in ['b,c']
by B5;
then B9:
x in [.b,c.]
by INTEGRA5:def 3, A1;
reconsider x =
x as
Real by B8;
(
b <= x &
x <= c )
by XXREAL_1:1, B9;
then B9c:
(
a <= x &
x <= c )
by XXREAL_0:2, A1;
dom (g | [.b,c.]) = [.b,c.]
by FUNCT_2:def 1;
then B11:
x in dom (g | [.b,c.])
by B9X, INTEGRA5:def 3, A1;
(h | (divset (D,i))) . x =
h . x
by B8, FUNCT_1:49
.=
((f | [.a,b.]) +* (g | [.b,c.])) . x
by A4, FUNCT_1:49, B9c, XXREAL_1:1
.=
(g | [.b,c.]) . x
by FUNCT_4:13, B11
.=
g . x
by B9, FUNCT_1:49
;
hence
(h | (divset (D,i))) . x = (g | (divset (D,i))) . x
by B8, FUNCT_1:49;
verum
end;
hence
h | (divset (D,i)) = g | (divset (D,i))
by FUNCT_2:12;
verum
end;
B3:
h2 | (divset (D,i)) =
g | (divset (D,i))
by B7, B5, FUNCT_1:51
.=
g1 | (divset (D,i))
by B5, FUNCT_1:51
;
(upper_volume (h2,D)) . i = (upper_bound (rng (g1 | (divset (D,i))))) * (vol (divset (D,i)))
by B3, INTEGRA1:def 6, B2;
hence
(upper_volume (h2,D)) . i = (upper_volume (g1,D)) . i
by INTEGRA1:def 6, B2;
verum
end;
hence
upper_volume (
h2,
D)
= upper_volume (
g1,
D)
by PARTFUN1:5, A8;
verum
end;
H1 . D =
upper_sum (
h2,
D)
by INTEGRA1:def 10
.=
Sum (upper_volume (g1,D))
by B4, INTEGRA1:def 8
.=
upper_sum (
g1,
D)
by INTEGRA1:def 8
.=
G . D
by INTEGRA1:def 10
;
hence
H1 . D = G . D
;
verum
end;
hence
H1 = G
by FUNCT_2:12;
verum
end;
C1: integral (h,['b,c']) =
integral h2
by INTEGRA5:def 2
.=
upper_integral h2
by INTEGRA1:def 17
.=
lower_bound (rng (upper_sum_set g1))
by A66, INTEGRA1:def 14
.=
upper_integral g1
by INTEGRA1:def 14
.=
integral g1
by INTEGRA1:def 17
.=
integral (g,['b,c'])
by INTEGRA5:def 2
;
reconsider h = h, f = f, g = g as PartFunc of REAL,REAL ;
A04:
a <= c
by A1, XXREAL_0:2;
A01:
h | ['a,c'] is bounded
by A1, A2, A3, A4, A5, Th18B;
A02:
dom h = REAL
by FUNCT_2:def 1;
b in [.a,c.]
by A1;
then A03:
b in ['a,c']
by INTEGRA5:def 3, A1, XXREAL_0:2;
integral (h,['a,c']) =
integral (h,a,c)
by INTEGRA5:def 4, A1, XXREAL_0:2
.=
(integral (h,a,b)) + (integral (h,b,c))
by INTEGRA6:17, A04, A0, A01, A03, A02
.=
(integral (f,['a,b'])) + (integral (h,b,c))
by B6, INTEGRA5:def 4, A1
.=
(integral (f,['a,b'])) + (integral (h,['b,c']))
by INTEGRA5:def 4, A1
;
hence
integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))
by C1; verum