let a, b, c be Real; for X being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f & c in ['a,b'] & b <> c holds
integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
let X be RealBanachSpace; for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f & c in ['a,b'] & b <> c holds
integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
let f be continuous PartFunc of REAL, the carrier of X; ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & b <> c implies integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
assume that
A1:
a <= b
and
A2:
['a,b'] c= dom f
and
A5:
c in ['a,b']
and
A6:
b <> c
; integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
reconsider AB = ['a,b'], AC = ['a,c'], CB = ['c,b'] as non empty closed_interval Subset of REAL ;
A7:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
then A8:
( a <= c & c <= b )
by A5, XXREAL_1:1;
then A9:
( ['a,c'] = [.a,c.] & ['c,b'] = [.c,b.] )
by INTEGRA5:def 3;
then
( [.c,b.] = [.(lower_bound [.c,b.]),(upper_bound [.c,b.]).] & [.a,c.] = [.(lower_bound [.a,c.]),(upper_bound [.a,c.]).] & [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] )
by A7, INTEGRA1:4;
then A11:
( upper_bound CB = b & lower_bound CB = c & upper_bound AC = c & lower_bound AC = a & upper_bound AB = b & lower_bound AB = a )
by A7, A9, INTEGRA1:5;
C1:
( f is_integrable_on AB & f is_integrable_on AC & f is_integrable_on CB )
by A1, A2, A8, Th1909;
consider FAB being Function of AB, the carrier of X such that
C3:
( FAB = f | AB & FAB is integrable )
by C1;
consider FAC being Function of AC, the carrier of X such that
C4:
( FAC = f | AC & FAC is integrable )
by C1;
consider FCB being Function of CB, the carrier of X such that
C5:
( FCB = f | CB & FCB is integrable )
by C1;
c < b
by A6, A8, XXREAL_0:1;
then
vol CB > 0
by A11, XREAL_1:50;
then consider PS2 being DivSequence of CB such that
A25:
( delta PS2 is convergent & lim (delta PS2) = 0 & ( for n being Element of NAT ex Tn being Division of CB st
( Tn divide_into_equal n + 1 & PS2 . n = Tn ) ) )
by INTEGRA6:16;
A27:
for i being Element of NAT st 2 <= i holds
ex S2i being Division of CB st
( S2i = PS2 . i & 2 <= len S2i )
defpred S1[ set , set ] means ex n being Nat ex e being Division of ['c,b'] st
( n = $1 & e = $2 & e = PS2 . (n + 2) );
A28:
for n being Element of NAT ex D being Element of divs CB st S1[n,D]
consider S2 being sequence of (divs CB) such that
A29:
for n being Element of NAT holds S1[n,S2 . n]
from FUNCT_2:sch 3(A28);
reconsider S2 = S2 as DivSequence of CB ;
defpred S2[ Element of NAT , set ] means ex S being Division of CB st
( S = S2 . $1 & $2 = S /^ 1 );
A31:
for i being Element of NAT ex T being Element of divs CB st S2[i,T]
proof
let i be
Element of
NAT ;
ex T being Element of divs CB st S2[i,T]
consider S being
Division of
CB such that A32:
(
S = S2 . i & 2
<= len S )
by A30;
set T =
S /^ 1;
A34:
1
<= len S
by A32, XXREAL_0:2;
2
- 1
<= (len S) - 1
by A32, XREAL_1:13;
then A35:
1
<= len (S /^ 1)
by A34, RFINSEQ:def 1;
then reconsider T =
S /^ 1 as non
empty increasing FinSequence of
REAL by A32, INTEGRA1:34, XXREAL_0:2;
len T in dom T
by A35, FINSEQ_3:25;
then
T . (len T) = S . ((len T) + 1)
by A34, RFINSEQ:def 1;
then
T . (len T) = S . (((len S) - 1) + 1)
by A34, RFINSEQ:def 1;
then A36:
T . (len T) = upper_bound CB
by INTEGRA1:def 2;
(
rng S c= CB &
rng T c= rng S )
by FINSEQ_5:33, INTEGRA1:def 2;
then
rng T c= CB
;
then
T is
Division of
CB
by A36, INTEGRA1:def 2;
then
T is
Element of
divs CB
by INTEGRA1:def 3;
hence
ex
T being
Element of
divs CB st
S2[
i,
T]
by A32;
verum
end;
consider T2 being DivSequence of CB such that
A38:
for i being Element of NAT holds S2[i,T2 . i]
from FUNCT_2:sch 3(A31);
A39:
for n being Element of NAT ex D being Division of CB st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )
proof
let n be
Element of
NAT ;
ex D being Division of CB st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )
reconsider D =
T2 . n as
Division of
CB ;
take
D
;
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )
consider E being
Division of
CB such that A40:
(
E = S2 . n &
T2 . n = E /^ 1 )
by A38;
A42:
ex
E1 being
Division of
CB st
(
E1 = S2 . n & 2
<= len E1 )
by A30;
then A43:
2
- 1
<= (len E) - 1
by A40, XREAL_1:13;
A44:
1
<= len E
by A40, A42, XXREAL_0:2;
then A45:
1
in dom E
by FINSEQ_3:25;
then
(
rng E c= CB &
E . 1
in rng E )
by FUNCT_1:def 3, INTEGRA1:def 2;
then A46:
c <= E . 1
by A9, XXREAL_1:1;
2
in dom E
by A40, A42, FINSEQ_3:25;
then A47:
E . 1
< E . 2
by A45, SEQM_3:def 1;
len D = (len E) - 1
by A40, A44, RFINSEQ:def 1;
then A48:
1
in dom D
by A43, FINSEQ_3:25;
then A49:
D . 1
= E . (1 + 1)
by A40, A44, RFINSEQ:def 1;
then A50:
c < D . 1
by A46, A47, XXREAL_0:2;
hence
(
D = T2 . n & ( for
i being
Element of
NAT st
i in dom D holds
c < D . i ) )
;
verum
end;
consider T1 being DivSequence of AC such that
A53:
( delta T1 is convergent & lim (delta T1) = 0 )
by INTEGRA4:11;
A54:
for n being Element of NAT ex D being Division of CB st
( D = T2 . n & 1 <= len D )
defpred S3[ Element of NAT , set ] means ex S1 being Division of AC ex S2 being Division of CB st
( S1 = T1 . $1 & S2 = T2 . $1 & $2 = S1 ^ S2 );
A61:
for i being Element of NAT ex T being Element of divs AB st S3[i,T]
proof
let i0 be
Element of
NAT ;
ex T being Element of divs AB st S3[i0,T]
reconsider S1 =
T1 . i0 as
Division of
AC ;
reconsider S2 =
T2 . i0 as
Division of
CB ;
set T =
S1 ^ S2;
ex
D being
Division of
CB st
(
D = T2 . i0 & 1
<= len D )
by A54;
then
len S2 in Seg (len S2)
;
then A62:
len S2 in dom S2
by FINSEQ_1:def 3;
A63:
rng S1 c= AC
by INTEGRA1:def 2;
then reconsider T =
S1 ^ S2 as non
empty increasing FinSequence of
REAL by SEQM_3:def 1;
rng S2 c= CB
by INTEGRA1:def 2;
then
(rng S1) \/ (rng S2) c= AC \/ CB
by A63, XBOOLE_1:13;
then
(rng S1) \/ (rng S2) c= [.a,b.]
by A8, A9, XXREAL_1:174;
then A92:
rng T c= AB
by A7, FINSEQ_1:31;
T . (len T) =
T . ((len S1) + (len S2))
by FINSEQ_1:22
.=
S2 . (len S2)
by A62, FINSEQ_1:def 7
.=
upper_bound AB
by A11, INTEGRA1:def 2
;
then reconsider T =
T as
Division of
AB by A92, INTEGRA1:def 2;
T is
Element of
divs AB
by INTEGRA1:def 3;
hence
ex
T being
Element of
divs AB st
S3[
i0,
T]
;
verum
end;
consider T being DivSequence of AB such that
A93:
for i being Element of NAT holds S3[i,T . i]
from FUNCT_2:sch 3(A61);
reconsider T = T as DivSequence of AB ;
reconsider T1 = T1 as DivSequence of AC ;
reconsider T2 = T2 as DivSequence of CB ;
set h1 = FAB;
set g1 = FAC;
set g2 = FCB;
set F1 = the middle_volume_Sequence of FAC,T1;
set F2 = the middle_volume_Sequence of FCB,T2;
B57:
( integral (f,c,b) = integral (f,CB) & integral (f,a,c) = integral (f,AC) )
by A9, INTEGR18:16;
A17:
( CB c= AB & AC c= AB )
by A7, A8, A9, XXREAL_1:34;
then
( CB c= dom f & AC c= dom f )
by A2;
then A57:
( integral (f,c,b) = integral FCB & integral (f,a,c) = integral FAC )
by B57, C4, C5, INTEGR18:9;
A95:
for i, k being Element of NAT
for S0 being Division of AC st S0 = T1 . i & k in Seg (len S0) holds
divset ((T . i),k) = divset ((T1 . i),k)
proof
let i,
k be
Element of
NAT ;
for S0 being Division of AC st S0 = T1 . i & k in Seg (len S0) holds
divset ((T . i),k) = divset ((T1 . i),k)let S0 be
Division of
AC;
( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) )
assume A96:
S0 = T1 . i
;
( not k in Seg (len S0) or divset ((T . i),k) = divset ((T1 . i),k) )
reconsider S =
T . i as
Division of
AB ;
A97:
divset (
(T1 . i),
k)
= [.(lower_bound (divset ((T1 . i),k))),(upper_bound (divset ((T1 . i),k))).]
by INTEGRA1:4;
consider S1 being
Division of
AC,
S2 being
Division of
CB such that A98:
(
S1 = T1 . i &
S2 = T2 . i )
and A99:
T . i = S1 ^ S2
by A93;
assume A100:
k in Seg (len S0)
;
divset ((T . i),k) = divset ((T1 . i),k)
then A101:
k in dom S1
by A96, A98, FINSEQ_1:def 3;
then A102:
k in dom S
by A99, FINSEQ_3:22;
A103:
divset (
(T . i),
k)
= [.(lower_bound (divset ((T . i),k))),(upper_bound (divset ((T . i),k))).]
by INTEGRA1:4;
A104:
now ( k <> 1 implies divset ((T . i),k) = divset ((T1 . i),k) )assume A106:
k <> 1
;
divset ((T . i),k) = divset ((T1 . i),k)
1
<= k
by A100, FINSEQ_1:1;
then
1
< k
by A106, XXREAL_0:1;
then
k - 1
in Seg (len S1)
by A96, A98, A100, FINSEQ_3:12;
then A109:
k - 1
in dom S1
by FINSEQ_1:def 3;
thus divset (
(T . i),
k) =
[.(S . (k - 1)),(upper_bound (divset ((T . i),k))).]
by A102, A103, A106, INTEGRA1:def 4
.=
[.(S . (k - 1)),(S . k).]
by A102, A106, INTEGRA1:def 4
.=
[.(S . (k - 1)),(S1 . k).]
by A99, A101, FINSEQ_1:def 7
.=
[.(S1 . (k - 1)),(S1 . k).]
by A99, A109, FINSEQ_1:def 7
.=
[.(lower_bound (divset ((T1 . i),k))),(S1 . k).]
by A98, A101, A106, INTEGRA1:def 4
.=
divset (
(T1 . i),
k)
by A98, A101, A97, A106, INTEGRA1:def 4
;
verum end;
now ( k = 1 implies divset ((T . i),k) = divset ((T1 . i),k) )assume A110:
k = 1
;
divset ((T . i),k) = divset ((T1 . i),k)hence divset (
(T . i),
k) =
[.(lower_bound AB),(upper_bound (divset ((T . i),k))).]
by A102, A103, INTEGRA1:def 4
.=
[.(lower_bound AB),(S . k).]
by A102, A110, INTEGRA1:def 4
.=
[.(lower_bound AB),(S1 . k).]
by A99, A101, FINSEQ_1:def 7
.=
[.(lower_bound (divset ((T1 . i),k))),(S1 . k).]
by A11, A98, A101, A110, INTEGRA1:def 4
.=
divset (
(T1 . i),
k)
by A98, A101, A97, A110, INTEGRA1:def 4
;
verum end;
hence
divset (
(T . i),
k)
= divset (
(T1 . i),
k)
by A104;
verum
end;
A112:
for i, k being Element of NAT
for S01 being Division of AC
for S02 being Division of CB st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
proof
let i,
k be
Element of
NAT ;
for S01 being Division of AC
for S02 being Division of CB st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)let S01 be
Division of
AC;
for S02 being Division of CB st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)let S02 be
Division of
CB;
( S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) implies divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )
assume A113:
(
S01 = T1 . i &
S02 = T2 . i )
;
( not k in Seg (len S02) or divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )
reconsider S =
T . i as
Division of
AB ;
consider S1 being
Division of
AC,
S2 being
Division of
CB such that A115:
(
S1 = T1 . i &
S2 = T2 . i )
and A117:
T . i = S1 ^ S2
by A93;
assume A118:
k in Seg (len S02)
;
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
then A119:
k in dom S2
by A113, A115, FINSEQ_1:def 3;
then A120:
(len S1) + k in dom S
by A117, FINSEQ_1:28;
A121:
divset (
(T2 . i),
k)
= [.(lower_bound (divset ((T2 . i),k))),(upper_bound (divset ((T2 . i),k))).]
by INTEGRA1:4;
A122:
divset (
(T . i),
((len S1) + k))
= [.(lower_bound (divset ((T . i),((len S1) + k)))),(upper_bound (divset ((T . i),((len S1) + k)))).]
by INTEGRA1:4;
A123:
now ( k <> 1 implies divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) )assume A125:
k <> 1
;
divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)A126:
1
<= k
by A118, FINSEQ_1:1;
then
1
< k
by A125, XXREAL_0:1;
then
k - 1
in Seg (len S2)
by A113, A115, A118, FINSEQ_3:12;
then A129:
k - 1
in dom S2
by FINSEQ_1:def 3;
A130:
1
+ 0 < k + (len S1)
by A126, XREAL_1:8;
hence divset (
(T . i),
((len S1) + k)) =
[.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).]
by A120, A122, INTEGRA1:def 4
.=
[.(S . (((len S1) + k) - 1)),(S . ((len S1) + k)).]
by A120, A130, INTEGRA1:def 4
.=
[.(S . ((len S1) + (k - 1))),(S2 . k).]
by A117, A119, FINSEQ_1:def 7
.=
[.(S2 . (k - 1)),(S2 . k).]
by A117, A129, FINSEQ_1:def 7
.=
[.(lower_bound (divset ((T2 . i),k))),(S2 . k).]
by A115, A119, A125, INTEGRA1:def 4
.=
divset (
(T2 . i),
k)
by A115, A119, A121, A125, INTEGRA1:def 4
;
verum end;
now ( k = 1 implies divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) )
len S1 in Seg (len S1)
by FINSEQ_1:3;
then A131:
len S1 in dom S1
by FINSEQ_1:def 3;
assume A132:
k = 1
;
divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)
len S1 <> 0
;
then A133:
(len S1) + k <> 1
by A132;
hence divset (
(T . i),
((len S1) + k)) =
[.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).]
by A120, A122, INTEGRA1:def 4
.=
[.(S1 . (len S1)),(upper_bound (divset ((T . i),((len S1) + k)))).]
by A117, A132, A131, FINSEQ_1:def 7
.=
[.(upper_bound AC),(upper_bound (divset ((T . i),((len S1) + k)))).]
by INTEGRA1:def 2
.=
[.(lower_bound CB),(S . ((len S1) + k)).]
by A11, A120, A133, INTEGRA1:def 4
.=
[.(lower_bound CB),(S2 . k).]
by A117, A119, FINSEQ_1:def 7
.=
[.(lower_bound (divset ((T2 . i),k))),(S2 . 1).]
by A115, A119, A132, INTEGRA1:def 4
.=
divset (
(T2 . i),
k)
by A115, A119, A121, A132, INTEGRA1:def 4
;
verum end;
hence
divset (
(T . i),
((len S01) + k))
= divset (
(T2 . i),
k)
by A113, A115, A123;
verum
end;
A134:
for i, k being Element of NAT
for S0 being Division of CB st S0 = T2 . i & k in Seg (len S0) holds
divset ((T2 . i),k) c= CB
A139:
for i, k being Element of NAT
for S0 being Division of AC st S0 = T1 . i & k in Seg (len S0) holds
divset ((T1 . i),k) c= AC
defpred S4[ Nat, set ] means ex q, q1, q2 being FinSequence of the carrier of X st
( q = $2 & q1 = the middle_volume_Sequence of FAC,T1 . $1 & q2 = the middle_volume_Sequence of FCB,T2 . $1 & q = q1 ^ q2 );
B12:
for k being Element of NAT ex y being Element of the carrier of X * st S4[k,y]
consider Sh1 being sequence of ( the carrier of X *) such that
B22:
for x being Element of NAT holds S4[x,Sh1 . x]
from FUNCT_2:sch 3(B12);
now for k being Element of NAT holds Sh1 . k is middle_volume of FAB,T . klet k be
Element of
NAT ;
Sh1 . k is middle_volume of FAB,T . kconsider q,
q1,
q2 being
FinSequence of the
carrier of
X such that B221:
(
q = Sh1 . k &
q1 = the
middle_volume_Sequence of
FAC,
T1 . k &
q2 = the
middle_volume_Sequence of
FCB,
T2 . k &
q = q1 ^ q2 )
by B22;
consider S1 being
Division of
AC,
S2 being
Division of
CB such that U1:
(
S1 = T1 . k &
S2 = T2 . k &
T . k = S1 ^ S2 )
by A93;
X1:
(
len ( the middle_volume_Sequence of FAC,T1 . k) = len (T1 . k) &
len ( the middle_volume_Sequence of FCB,T2 . k) = len (T2 . k) )
by INTEGR18:def 1;
then B226:
(
len (Sh1 . k) = (len (T1 . k)) + (len (T2 . k)) &
len (T . k) = (len (T1 . k)) + (len (T2 . k)) )
by U1, B221, FINSEQ_1:22;
for
i being
Nat st
i in dom (T . k) holds
ex
c being
Point of
X st
(
c in rng (FAB | (divset ((T . k),i))) &
(Sh1 . k) . i = (vol (divset ((T . k),i))) * c )
proof
let i be
Nat;
( i in dom (T . k) implies ex c being Point of X st
( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c ) )
assume
i in dom (T . k)
;
ex c being Point of X st
( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c )
per cases then
( i in dom S1 or ex n being Nat st
( n in dom S2 & i = (len S1) + n ) )
by U1, FINSEQ_1:25;
suppose VC1:
i in dom S1
;
ex c being Point of X st
( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c )then VC3:
ex
c being
Point of
X st
(
c in rng (FAC | (divset ((T1 . k),i))) &
( the middle_volume_Sequence of FAC,T1 . k) . i = (vol (divset ((T1 . k),i))) * c )
by INTEGR18:def 1, U1;
VC41:
i in dom ( the middle_volume_Sequence of FAC,T1 . k)
by VC1, U1, X1, FINSEQ_3:29;
V1:
i in Seg (len S1)
by VC1, FINSEQ_1:def 3;
V6:
divset (
(T1 . k),
i)
= divset (
(T . k),
i)
by V1, A95, U1;
divset (
(T1 . k),
i)
c= AC
by V1, U1, A139;
then V4:
divset (
(T1 . k),
i)
c= AB
by A17;
(f | AC) | (divset ((T1 . k),i)) = f | (divset ((T1 . k),i))
by RELAT_1:74, V1, U1, A139;
then
FAC | (divset ((T1 . k),i)) = FAB | (divset ((T . k),i))
by C3, C4, V6, RELAT_1:74, V4;
hence
ex
c being
Point of
X st
(
c in rng (FAB | (divset ((T . k),i))) &
(Sh1 . k) . i = (vol (divset ((T . k),i))) * c )
by VC3, VC41, B221, FINSEQ_1:def 7, V6;
verum end; suppose
ex
n being
Nat st
(
n in dom S2 &
i = (len S1) + n )
;
ex c being Point of X st
( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c )then consider n being
Nat such that C20:
(
n in dom S2 &
i = (len S1) + n )
;
VC3:
(
i = (len ( the middle_volume_Sequence of FAC,T1 . k)) + n & ex
c being
Point of
X st
(
c in rng (FCB | (divset ((T2 . k),n))) &
( the middle_volume_Sequence of FCB,T2 . k) . n = (vol (divset ((T2 . k),n))) * c ) )
by INTEGR18:def 1, U1, C20;
V1:
(
n in dom ( the middle_volume_Sequence of FCB,T2 . k) &
n in Seg (len S2) )
by C20, U1, X1, FINSEQ_1:def 3, FINSEQ_3:29;
VC5:
divset (
(T2 . k),
n)
= divset (
(T . k),
i)
by C20, V1, A112, U1;
divset (
(T2 . k),
n)
c= CB
by V1, U1, A134;
then V4:
divset (
(T2 . k),
n)
c= AB
by A17;
(f | CB) | (divset ((T2 . k),n)) = f | (divset ((T2 . k),n))
by RELAT_1:74, V1, U1, A134;
then
FCB | (divset ((T2 . k),n)) = FAB | (divset ((T . k),i))
by C3, C5, VC5, RELAT_1:74, V4;
hence
ex
c being
Point of
X st
(
c in rng (FAB | (divset ((T . k),i))) &
(Sh1 . k) . i = (vol (divset ((T . k),i))) * c )
by VC3, V1, B221, FINSEQ_1:def 7, VC5;
verum end; end;
end; hence
Sh1 . k is
middle_volume of
FAB,
T . k
by B226, INTEGR18:def 1;
verum end;
then reconsider F = Sh1 as middle_volume_Sequence of FAB,T by INTEGR18:def 3;
A164:
for i being Nat holds middle_sum (FAB,(F . i)) = (middle_sum (FAC,( the middle_volume_Sequence of FAC,T1 . i))) + (middle_sum (FCB,( the middle_volume_Sequence of FCB,T2 . i)))
proof
let i be
Nat;
middle_sum (FAB,(F . i)) = (middle_sum (FAC,( the middle_volume_Sequence of FAC,T1 . i))) + (middle_sum (FCB,( the middle_volume_Sequence of FCB,T2 . i)))
i is
Element of
NAT
by ORDINAL1:def 12;
then
ex
q,
q1,
q2 being
FinSequence of the
carrier of
X st
(
q = Sh1 . i &
q1 = the
middle_volume_Sequence of
FAC,
T1 . i &
q2 = the
middle_volume_Sequence of
FCB,
T2 . i &
q = q1 ^ q2 )
by B22;
hence
middle_sum (
FAB,
(F . i))
= (middle_sum (FAC,( the middle_volume_Sequence of FAC,T1 . i))) + (middle_sum (FCB,( the middle_volume_Sequence of FCB,T2 . i)))
by RLVECT_1:41;
verum
end;
now for i being Nat holds (middle_sum (FAB,F)) . i = ((middle_sum (FAC, the middle_volume_Sequence of FAC,T1)) . i) + ((middle_sum (FCB, the middle_volume_Sequence of FCB,T2)) . i)let i be
Nat;
(middle_sum (FAB,F)) . i = ((middle_sum (FAC, the middle_volume_Sequence of FAC,T1)) . i) + ((middle_sum (FCB, the middle_volume_Sequence of FCB,T2)) . i)thus (middle_sum (FAB,F)) . i =
middle_sum (
FAB,
(F . i))
by INTEGR18:def 4
.=
(middle_sum (FAC,( the middle_volume_Sequence of FAC,T1 . i))) + (middle_sum (FCB,( the middle_volume_Sequence of FCB,T2 . i)))
by A164
.=
((middle_sum (FAC, the middle_volume_Sequence of FAC,T1)) . i) + (middle_sum (FCB,( the middle_volume_Sequence of FCB,T2 . i)))
by INTEGR18:def 4
.=
((middle_sum (FAC, the middle_volume_Sequence of FAC,T1)) . i) + ((middle_sum (FCB, the middle_volume_Sequence of FCB,T2)) . i)
by INTEGR18:def 4
;
verum end;
then A165:
middle_sum (FAB,F) = (middle_sum (FAC, the middle_volume_Sequence of FAC,T1)) + (middle_sum (FCB, the middle_volume_Sequence of FCB,T2))
by NORMSP_1:def 2;
reconsider XAB = chi (AB,AB) as PartFunc of AB,REAL ;
reconsider XAC = chi (AC,AC) as PartFunc of AC,REAL ;
reconsider XCB = chi (CB,CB) as PartFunc of CB,REAL ;
A172:
now for e being Real st e > 0 holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((delta T2) . n) - 0).| < elet e be
Real;
( e > 0 implies ex m being Nat st
for n being Nat st m <= n holds
|.(((delta T2) . n) - 0).| < e )assume A173:
e > 0
;
ex m being Nat st
for n being Nat st m <= n holds
|.(((delta T2) . n) - 0).| < ethen consider m being
Nat such that A174:
for
n being
Nat st
m <= n holds
|.(((delta S2) . n) - 0).| < e / 2
by A168, XREAL_1:215;
take m =
m;
for n being Nat st m <= n holds
|.(((delta T2) . n) - 0).| < eA175:
e / 2
< e
by A173, XREAL_1:216;
let n be
Nat;
( m <= n implies |.(((delta T2) . n) - 0).| < e )X1:
n in NAT
by ORDINAL1:def 12;
assume
m <= n
;
|.(((delta T2) . n) - 0).| < ethen
|.(((delta S2) . n) - 0).| < e / 2
by A174;
then
(
0 <= delta (S2 . n) &
|.(delta (S2 . n)).| < e / 2 )
by X1, INTEGRA3:9, INTEGRA3:def 2;
then A177:
max (rng (upper_volume (XCB,(S2 . n)))) < e / 2
by ABSVALUE:def 1;
reconsider S2n =
S2 . n as
Division of
CB ;
A178:
for
y being
Real st
y in rng (upper_volume (XCB,(T2 . n))) holds
y < e
proof
reconsider D =
T2 . n as
Division of
CB ;
let y be
Real;
( y in rng (upper_volume (XCB,(T2 . n))) implies y < e )
assume
y in rng (upper_volume (XCB,(T2 . n)))
;
y < e
then consider x being
object such that A179:
(
x in dom (upper_volume (XCB,(T2 . n))) &
y = (upper_volume (XCB,(T2 . n))) . x )
by FUNCT_1:def 3;
reconsider i =
x as
Nat by A179;
A181:
x in Seg (len (upper_volume (XCB,(T2 . n))))
by A179, FINSEQ_1:def 3;
X1:
n in NAT
by ORDINAL1:def 12;
then consider E1 being
Division of
CB such that A182:
(
E1 = S2 . n & 2
<= len E1 )
by A30;
set i1 =
i + 1;
consider E being
Division of
CB such that A184:
E = S2 . n
and A185:
T2 . n = E /^ 1
by A38, X1;
A186:
1
<= len E1
by A182, XXREAL_0:2;
then A187:
len D = (len E) - 1
by A184, A185, A182, RFINSEQ:def 1;
A188:
len (upper_volume (XCB,(T2 . n))) = len D
by INTEGRA1:def 6;
then A189:
dom (upper_volume (XCB,(T2 . n))) = dom D
by FINSEQ_3:29;
then A203:
y = (upper_bound (rng (XCB | (divset ((T2 . n),i))))) * (vol (divset ((T2 . n),i)))
by A179, INTEGRA1:def 6;
A207:
i in dom D
by A181, A188, FINSEQ_1:def 3;
A196:
( 1
in dom E & 2
in dom E )
by A184, A182, A186, FINSEQ_3:25;
then XX2:
(
E . 2
= upper_bound (divset ((S2 . n),2)) &
E . (2 - 1) = lower_bound (divset ((S2 . n),2)) &
lower_bound CB = lower_bound (divset ((S2 . n),1)) &
E . 1
= upper_bound (divset ((S2 . n),1)) )
by A184, INTEGRA1:def 4;
XX6:
(
vol (divset ((S2 . n),1)) = (upper_volume (XCB,(S2 . n))) . 1 &
vol (divset ((S2 . n),2)) = (upper_volume (XCB,(S2 . n))) . 2 )
by A184, A196, INTEGRA1:20;
XX1:
(
len (upper_volume (XCB,(S2 . n))) = len E &
len (upper_volume (XCB,(S2 . n))) = (len D) + 1 )
by A184, A187, INTEGRA1:def 6;
then
1
<= len (upper_volume (XCB,(S2 . n)))
by NAT_1:11;
then
( 1
in dom (upper_volume (XCB,(S2 . n))) & 2
in dom (upper_volume (XCB,(S2 . n))) )
by XX1, A184, A182, FINSEQ_3:25;
then
(
(upper_volume (XCB,(S2 . n))) . 1
in rng (upper_volume (XCB,(S2 . n))) &
(upper_volume (XCB,(S2 . n))) . 2
in rng (upper_volume (XCB,(S2 . n))) )
by FUNCT_1:def 3;
then
(
(upper_volume (XCB,(S2 . n))) . 1
<= max (rng (upper_volume (XCB,(S2 . n)))) &
(upper_volume (XCB,(S2 . n))) . 2
<= max (rng (upper_volume (XCB,(S2 . n)))) )
by XXREAL_2:def 8;
then A191:
(
vol (divset ((S2 . n),1)) < e / 2 &
vol (divset ((S2 . n),2)) < e / 2 )
by XX6, A177, XXREAL_0:2;
XX4:
(
divset (
(S2 . n),2)
= [.(lower_bound (divset ((S2 . n),2))),(upper_bound (divset ((S2 . n),2))).] &
divset (
(T2 . n),
i)
= [.(lower_bound (divset ((T2 . n),i))),(upper_bound (divset ((T2 . n),i))).] &
divset (
(S2 . n),
(i + 1))
= [.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).] )
by INTEGRA1:4;
XX5:
D . i = E . (i + 1)
by A184, A185, A182, A186, A207, RFINSEQ:def 1;
A209:
dom (upper_volume (XCB,(S2 . n))) = dom E
by XX1, FINSEQ_3:29;
i + 1
in Seg (len (upper_volume (XCB,(S2 . n))))
by XX1, A181, A188, FINSEQ_1:60;
then A205:
i + 1
in dom (upper_volume (XCB,(S2 . n)))
by FINSEQ_1:def 3;
A190:
now ( i = 1 implies y < e )assume A192:
i = 1
;
y < ethen XX3:
(
lower_bound CB = lower_bound (divset ((T2 . n),1)) &
D . 1
= upper_bound (divset ((T2 . n),1)) )
by A207, INTEGRA1:def 4;
y = vol (divset ((T2 . n),1))
by A179, A189, A192, INTEGRA1:20;
then
y = (vol (divset ((S2 . n),2))) + (vol (divset ((S2 . n),1)))
by A192, XX3, XX5, XX2;
then
y < (e / 2) + (e / 2)
by A191, XREAL_1:8;
hence
y < e
;
verum end;
now ( i <> 1 implies y < e )assume A210:
i <> 1
;
y < ethen XX7:
(
D . (i - 1) = lower_bound (divset ((T2 . n),i)) &
D . i = upper_bound (divset ((T2 . n),i)) )
by A207, INTEGRA1:def 4;
B211:
1
<= i
by A179, FINSEQ_3:25;
then reconsider i9 =
i - 1 as
Nat ;
A211:
1
< i
by A210, B211, XXREAL_0:1;
then
i9 in Seg (len D)
by A181, A188, FINSEQ_3:12;
then
i9 in dom D
by FINSEQ_1:def 3;
then XX9:
D . (i - 1) = E . (i9 + 1)
by A184, A185, A182, A186, RFINSEQ:def 1;
1
+ 1
< i + 1
by A211, XREAL_1:8;
then
i + 1
<> 1
;
then
(
E . ((i + 1) - 1) = lower_bound (divset ((S2 . n),(i + 1))) &
E . (i + 1) = upper_bound (divset ((S2 . n),(i + 1))) )
by A184, A205, A209, INTEGRA1:def 4;
then
y = (upper_volume (XCB,(S2 . n))) . (i + 1)
by XX5, XX4, XX7, XX9, A203, A184, A205, A209, INTEGRA1:def 6;
then
y in rng (upper_volume (XCB,(S2 . n)))
by A205, FUNCT_1:def 3;
then
y <= max (rng (upper_volume (XCB,(S2 . n))))
by XXREAL_2:def 8;
then
y < e / 2
by A177, XXREAL_0:2;
hence
y < e
by A175, XXREAL_0:2;
verum end;
hence
y < e
by A190;
verum
end; X1:
n in NAT
by ORDINAL1:def 12;
max (rng (upper_volume (XCB,(T2 . n)))) in rng (upper_volume (XCB,(T2 . n)))
by XXREAL_2:def 8;
then
(
0 <= delta (T2 . n) &
delta (T2 . n) < e )
by A178, INTEGRA3:9;
then
|.(delta (T2 . n)).| < e
by ABSVALUE:def 1;
hence
|.(((delta T2) . n) - 0).| < e
by INTEGRA3:def 2, X1;
verum end;
then A215:
delta T2 is convergent
by SEQ_2:def 6;
then
lim (delta T2) = 0
by A172, SEQ_2:def 7;
then A217:
( middle_sum (FCB, the middle_volume_Sequence of FCB,T2) is convergent & lim (middle_sum (FCB, the middle_volume_Sequence of FCB,T2)) = integral FCB )
by A215, C5, INTEGR18:def 6;
A218:
now for e being Real st 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((delta T) . m) - 0).| < elet e be
Real;
( 0 < e implies ex n being Nat st
for m being Nat st n <= m holds
|.(((delta T) . m) - 0).| < e )assume A219:
0 < e
;
ex n being Nat st
for m being Nat st n <= m holds
|.(((delta T) . m) - 0).| < ethen consider n1 being
Nat such that A220:
for
m being
Nat st
n1 <= m holds
|.(((delta T1) . m) - 0).| < e
by A53, SEQ_2:def 7;
consider n2 being
Nat such that A221:
for
m being
Nat st
n2 <= m holds
|.(((delta T2) . m) - 0).| < e
by A172, A219;
reconsider n =
max (
n1,
n2) as
Nat by TARSKI:1;
take n =
n;
for m being Nat st n <= m holds
|.(((delta T) . m) - 0).| < elet m be
Nat;
( n <= m implies |.(((delta T) . m) - 0).| < e )assume A222:
n <= m
;
|.(((delta T) . m) - 0).| < eX1:
m in NAT
by ORDINAL1:def 12;
(
n1 <= n &
n2 <= n )
by XXREAL_0:25;
then
(
n1 <= m &
n2 <= m )
by A222, XXREAL_0:2;
then
(
|.(((delta T1) . m) - 0).| < e &
|.(((delta T2) . m) - 0).| < e )
by A220, A221;
then
(
|.(delta (T1 . m)).| < e &
|.(delta (T2 . m)).| < e )
by X1, INTEGRA3:def 2;
then A224:
(
max (rng (upper_volume (XCB,(T2 . m)))) < e &
max (rng (upper_volume (XAC,(T1 . m)))) < e )
by ABSVALUE:def 1, INTEGRA3:9;
A227:
for
r being
Real st
r in rng (upper_volume (XAB,(T . m))) holds
r < e
proof
reconsider Tm =
T . m as
Division of
AB ;
let y be
Real;
( y in rng (upper_volume (XAB,(T . m))) implies y < e )
assume
y in rng (upper_volume (XAB,(T . m)))
;
y < e
then consider x being
object such that A228:
(
x in dom (upper_volume (XAB,(T . m))) &
y = (upper_volume (XAB,(T . m))) . x )
by FUNCT_1:def 3;
reconsider i =
x as
Nat by A228;
A230:
x in Seg (len (upper_volume (XAB,(T . m))))
by A228, FINSEQ_1:def 3;
then A231:
1
<= i
by FINSEQ_1:1;
A232:
len (upper_volume (XAB,(T . m))) = len Tm
by INTEGRA1:def 6;
then A233:
i <= len Tm
by A230, FINSEQ_1:1;
dom (upper_volume (XAB,(T . m))) = dom Tm
by A232, FINSEQ_3:29;
then A234:
y = (upper_bound (rng (XAB | (divset ((T . m),i))))) * (vol (divset ((T . m),i)))
by A228, INTEGRA1:def 6;
consider S1 being
Division of
AC,
S2 being
Division of
CB such that A235:
(
S1 = T1 . m &
S2 = T2 . m )
and A237:
T . m = S1 ^ S2
by A93, X1;
A238:
len Tm = (len S1) + (len S2)
by A237, FINSEQ_1:22;
per cases
( i <= len S1 or i > len S1 )
;
suppose
i <= len S1
;
y < ethen A239:
i in Seg (len S1)
by A231;
then A240:
i in dom S1
by FINSEQ_1:def 3;
len (upper_volume (XAC,(T1 . m))) = len S1
by A235, INTEGRA1:def 6;
then A241:
dom (upper_volume (XAC,(T1 . m))) = dom S1
by FINSEQ_3:29;
A242:
divset (
(T1 . m),
i)
= divset (
(T . m),
i)
by X1, A95, A235, A239;
A243:
divset (
(T1 . m),
i)
c= AC
by X1, A139, A235, A239;
then
divset (
(T1 . m),
i)
c= AB
by A17;
then
XAC | (divset ((T1 . m),i)) = XAB | (divset ((T . m),i))
by A242, A243, INTEGRA6:4;
then
y = (upper_volume (XAC,(T1 . m))) . i
by A234, A235, A240, A242, INTEGRA1:def 6;
then
y in rng (upper_volume (XAC,(T1 . m)))
by A240, A241, FUNCT_1:def 3;
then
y <= max (rng (upper_volume (XAC,(T1 . m))))
by XXREAL_2:def 8;
hence
y < e
by A224, XXREAL_0:2;
verum end; suppose
i > len S1
;
y < ethen A244:
(len S1) + 1
<= i
by NAT_1:13;
then consider k being
Nat such that A245:
((len S1) + 1) + k = i
by NAT_1:10;
set i1 = 1
+ k;
A246:
i - (len S1) <= len S2
by A238, A233, XREAL_1:20;
1
+ k = i - (len S1)
by A245;
then
1
<= 1
+ k
by A244, XREAL_1:19;
then A247:
1
+ k in Seg (len S2)
by A245, A246;
then A248:
1
+ k in dom S2
by FINSEQ_1:def 3;
A249:
divset (
(T2 . m),
(1 + k))
= divset (
(T . m),
((len S1) + (1 + k)))
by X1, A112, A235, A247;
A250:
divset (
(T2 . m),
(1 + k))
c= CB
by X1, A134, A235, A247;
then
divset (
(T2 . m),
(1 + k))
c= AB
by A17;
then
y = (upper_bound (rng (XCB | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k))))
by A234, A245, A249, A250, INTEGRA6:4;
then A251:
y = (upper_volume (XCB,(T2 . m))) . (1 + k)
by A235, A248, INTEGRA1:def 6;
len (upper_volume (XCB,(T2 . m))) = len S2
by A235, INTEGRA1:def 6;
then
1
+ k in dom (upper_volume (XCB,(T2 . m)))
by A247, FINSEQ_1:def 3;
then
y in rng (upper_volume (XCB,(T2 . m)))
by A251, FUNCT_1:def 3;
then
y <= max (rng (upper_volume (XCB,(T2 . m))))
by XXREAL_2:def 8;
hence
y < e
by A224, XXREAL_0:2;
verum end; end;
end;
max (rng (upper_volume (XAB,(T . m)))) in rng (upper_volume (XAB,(T . m)))
by XXREAL_2:def 8;
then
delta (T . m) < e
by A227;
then
|.(delta (T . m)).| < e
by INTEGRA3:9, ABSVALUE:def 1;
hence
|.(((delta T) . m) - 0).| < e
by X1, INTEGRA3:def 2;
verum end;
then A253:
delta T is convergent
by SEQ_2:def 6;
then B255:
lim (delta T) = 0
by A218, SEQ_2:def 7;
A282:
( middle_sum (FAC, the middle_volume_Sequence of FAC,T1) is convergent & lim (middle_sum (FAC, the middle_volume_Sequence of FAC,T1)) = integral FAC )
by A53, C4, INTEGR18:def 6;
integral (f,a,b) =
integral (f,AB)
by A7, INTEGR18:16
.=
integral FAB
by A2, C3, INTEGR18:9
.=
lim (middle_sum (FAB,F))
by B255, A253, C3, INTEGR18:def 6
;
hence
integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
by A57, A165, A282, A217, NORMSP_1:25; verum