let a, b, c be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 )_{1}[ 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 S_{1}[n,D]

A29: for n being Element of NAT holds S_{1}[n,S2 . n]
from FUNCT_2:sch 3(A28);

reconsider S2 = S2 as DivSequence of CB ;

defpred S_{2}[ Element of NAT , set ] means ex S being Division of CB st

( S = S2 . $1 & $2 = S /^ 1 );

_{2}[i,T]

A38: for i being Element of NAT holds S_{2}[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 ) )

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 )_{3}[ 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 S_{3}[i,T]

A93: for i being Element of NAT holds S_{3}[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)

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)

for S0 being Division of CB st S0 = T2 . i & k in Seg (len S0) holds

divset ((T2 . i),k) c= CB

for S0 being Division of AC st S0 = T1 . i & k in Seg (len S0) holds

divset ((T1 . i),k) c= AC_{4}[ 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 S_{4}[k,y]

B22: for x being Element of NAT holds S_{4}[x,Sh1 . x]
from FUNCT_2:sch 3(B12);

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)))

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 ;

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;

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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 )

proof

defpred S
let i be Element of NAT ; :: thesis: ( 2 <= i implies ex S2i being Division of CB st

( S2i = PS2 . i & 2 <= len S2i ) )

assume A22: 2 <= i ; :: thesis: ex S2i being Division of CB st

( S2i = PS2 . i & 2 <= len S2i )

consider Tn being Division of CB such that

A23: ( Tn divide_into_equal i + 1 & PS2 . i = Tn ) by A25;

take Tn ; :: thesis: ( Tn = PS2 . i & 2 <= len Tn )

thus Tn = PS2 . i by A23; :: thesis: 2 <= len Tn

i <= len Tn by NAT_1:11, A23;

hence 2 <= len Tn by A22, XXREAL_0:2; :: thesis: verum

end;( S2i = PS2 . i & 2 <= len S2i ) )

assume A22: 2 <= i ; :: thesis: ex S2i being Division of CB st

( S2i = PS2 . i & 2 <= len S2i )

consider Tn being Division of CB such that

A23: ( Tn divide_into_equal i + 1 & PS2 . i = Tn ) by A25;

take Tn ; :: thesis: ( Tn = PS2 . i & 2 <= len Tn )

thus Tn = PS2 . i by A23; :: thesis: 2 <= len Tn

i <= len Tn by NAT_1:11, A23;

hence 2 <= len Tn by A22, XXREAL_0:2; :: thesis: verum

( n = $1 & e = $2 & e = PS2 . (n + 2) );

A28: for n being Element of NAT ex D being Element of divs CB st S

proof

consider S2 being sequence of (divs CB) such that
let n be Element of NAT ; :: thesis: ex D being Element of divs CB st S_{1}[n,D]

reconsider D = PS2 . (n + 2) as Element of divs CB by INTEGRA1:def 3;

take D ; :: thesis: S_{1}[n,D]

thus S_{1}[n,D]
; :: thesis: verum

end;reconsider D = PS2 . (n + 2) as Element of divs CB by INTEGRA1:def 3;

take D ; :: thesis: S

thus S

A29: for n being Element of NAT holds S

reconsider S2 = S2 as DivSequence of CB ;

defpred S

( S = S2 . $1 & $2 = S /^ 1 );

A30: now :: thesis: for i being Element of NAT ex S2i being Division of CB st

( S2i = S2 . i & 2 <= len S2i )

A31:
for i being Element of NAT ex T being Element of divs CB st S( S2i = S2 . i & 2 <= len S2i )

let i be Element of NAT ; :: thesis: ex S2i being Division of CB st

( S2i = S2 . i & 2 <= len S2i )

ex n being Nat ex e being Division of CB st

( n = i & e = S2 . i & e = PS2 . (n + 2) ) by A29;

hence ex S2i being Division of CB st

( S2i = S2 . i & 2 <= len S2i ) by A27, NAT_1:11; :: thesis: verum

end;( S2i = S2 . i & 2 <= len S2i )

ex n being Nat ex e being Division of CB st

( n = i & e = S2 . i & e = PS2 . (n + 2) ) by A29;

hence ex S2i being Division of CB st

( S2i = S2 . i & 2 <= len S2i ) by A27, NAT_1:11; :: thesis: verum

proof

consider T2 being DivSequence of CB such that
let i be Element of NAT ; :: thesis: ex T being Element of divs CB st S_{2}[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 S_{2}[i,T]
by A32; :: thesis: verum

end;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 S

A38: for i being Element of NAT holds S

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

consider T1 being DivSequence of AC such that
let n be Element of NAT ; :: thesis: 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 ; :: thesis: ( 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;

c < D . i ) ) ; :: thesis: verum

end;( 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 ; :: thesis: ( 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;

now :: thesis: for i being Element of NAT st i in dom D holds

( ( i <> 1 implies c < D . i ) & c < D . i )

hence
( D = T2 . n & ( for i being Element of NAT st i in dom D holds ( ( i <> 1 implies c < D . i ) & c < D . i )

let i be Element of NAT ; :: thesis: ( i in dom D implies ( ( i <> 1 implies c < D . i ) & c < D . i ) )

assume A51: i in dom D ; :: thesis: ( ( i <> 1 implies c < D . i ) & c < D . i )

then A52: 1 <= i by FINSEQ_3:25;

end;assume A51: i in dom D ; :: thesis: ( ( i <> 1 implies c < D . i ) & c < D . i )

then A52: 1 <= i by FINSEQ_3:25;

hereby :: thesis: c < D . i

hence
c < D . i
by A49, A46, A47, XXREAL_0:2; :: thesis: verumassume
i <> 1
; :: thesis: c < D . i

then 1 < i by A52, XXREAL_0:1;

then D . 1 < D . i by A48, A51, SEQM_3:def 1;

hence c < D . i by A50, XXREAL_0:2; :: thesis: verum

end;then 1 < i by A52, XXREAL_0:1;

then D . 1 < D . i by A48, A51, SEQM_3:def 1;

hence c < D . i by A50, XXREAL_0:2; :: thesis: verum

c < D . i ) ) ; :: thesis: verum

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 )

proof

defpred S
let n be Element of NAT ; :: thesis: ex D being Division of CB st

( D = T2 . n & 1 <= len D )

reconsider D = T2 . n as Division of CB ;

take D ; :: thesis: ( D = T2 . n & 1 <= len D )

consider E being Division of CB such that

A55: ( E = S2 . n & T2 . n = E /^ 1 ) by A38;

ex E1 being Division of CB st

( E1 = S2 . n & 2 <= len E1 ) by A30;

then ( 1 <= len E & 2 - 1 <= (len E) - 1 ) by A55, XREAL_1:13, XXREAL_0:2;

hence ( D = T2 . n & 1 <= len D ) by A55, RFINSEQ:def 1; :: thesis: verum

end;( D = T2 . n & 1 <= len D )

reconsider D = T2 . n as Division of CB ;

take D ; :: thesis: ( D = T2 . n & 1 <= len D )

consider E being Division of CB such that

A55: ( E = S2 . n & T2 . n = E /^ 1 ) by A38;

ex E1 being Division of CB st

( E1 = S2 . n & 2 <= len E1 ) by A30;

then ( 1 <= len E & 2 - 1 <= (len E) - 1 ) by A55, XREAL_1:13, XXREAL_0:2;

hence ( D = T2 . n & 1 <= len D ) by A55, RFINSEQ:def 1; :: thesis: verum

( S1 = T1 . $1 & S2 = T2 . $1 & $2 = S1 ^ S2 );

A61: for i being Element of NAT ex T being Element of divs AB st S

proof

consider T being DivSequence of AB such that
let i0 be Element of NAT ; :: thesis: ex T being Element of divs AB st S_{3}[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;

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 S_{3}[i0,T]
; :: thesis: verum

end;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;

now :: thesis: for i, j being Nat st i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j holds

(S1 ^ S2) . i < (S1 ^ S2) . j

then reconsider T = S1 ^ S2 as non empty increasing FinSequence of REAL by SEQM_3:def 1;(S1 ^ S2) . i < (S1 ^ S2) . j

let i, j be Nat; :: thesis: ( i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j implies (S1 ^ S2) . i < (S1 ^ S2) . j )

assume that

A64: ( i in dom (S1 ^ S2) & j in dom (S1 ^ S2) ) and

A66: i < j ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j

A67: ( 1 <= i & i <= len (S1 ^ S2) & 1 <= j & j <= len (S1 ^ S2) ) by A64, FINSEQ_3:25;

then ( i <= (len S1) + (len S2) & j <= (len S1) + (len S2) ) by FINSEQ_1:22;

then A71: ( i - (len S1) <= len S2 & j - (len S1) <= len S2 ) by XREAL_1:20;

A79: i - (len S1) < j - (len S1) by A66, XREAL_1:14;

end;assume that

A64: ( i in dom (S1 ^ S2) & j in dom (S1 ^ S2) ) and

A66: i < j ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j

A67: ( 1 <= i & i <= len (S1 ^ S2) & 1 <= j & j <= len (S1 ^ S2) ) by A64, FINSEQ_3:25;

then ( i <= (len S1) + (len S2) & j <= (len S1) + (len S2) ) by FINSEQ_1:22;

then A71: ( i - (len S1) <= len S2 & j - (len S1) <= len S2 ) by XREAL_1:20;

A79: i - (len S1) < j - (len S1) by A66, XREAL_1:14;

A70: now :: thesis: ( j > len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )

assume A72:
j > len S1
; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j

then A73: (S1 ^ S2) . j = S2 . (j - (len S1)) by A67, FINSEQ_1:24;

A74: (len S1) + 1 <= j by A72, NAT_1:13;

then consider m being Nat such that

A75: ((len S1) + 1) + m = j by NAT_1:10;

1 + m = j - (len S1) by A75;

then A76: j - (len S1) in dom S2 by A71, A74, XREAL_1:19, FINSEQ_3:25;

end;then A73: (S1 ^ S2) . j = S2 . (j - (len S1)) by A67, FINSEQ_1:24;

A74: (len S1) + 1 <= j by A72, NAT_1:13;

then consider m being Nat such that

A75: ((len S1) + 1) + m = j by NAT_1:10;

1 + m = j - (len S1) by A75;

then A76: j - (len S1) in dom S2 by A71, A74, XREAL_1:19, FINSEQ_3:25;

A77: now :: thesis: ( i > len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )

assume A80:
i > len S1
; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j

then A81: (len S1) + 1 <= i by NAT_1:13;

then consider m being Nat such that

A82: ((len S1) + 1) + m = i by NAT_1:10;

1 + m = i - (len S1) by A82;

then A83: i - (len S1) in dom S2 by A71, A81, XREAL_1:19, FINSEQ_3:25;

(S1 ^ S2) . i = S2 . (i - (len S1)) by A67, A80, FINSEQ_1:24;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A79, A83, SEQM_3:def 1; :: thesis: verum

end;then A81: (len S1) + 1 <= i by NAT_1:13;

then consider m being Nat such that

A82: ((len S1) + 1) + m = i by NAT_1:10;

1 + m = i - (len S1) by A82;

then A83: i - (len S1) in dom S2 by A71, A81, XREAL_1:19, FINSEQ_3:25;

(S1 ^ S2) . i = S2 . (i - (len S1)) by A67, A80, FINSEQ_1:24;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A79, A83, SEQM_3:def 1; :: thesis: verum

now :: thesis: ( i <= len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )

hence
(S1 ^ S2) . i < (S1 ^ S2) . j
by A77; :: thesis: verumassume
i <= len S1
; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j

then A84: i in dom S1 by A67, FINSEQ_3:25;

then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def 7;

then (S1 ^ S2) . i in rng S1 by A84, FUNCT_1:def 3;

then A85: (S1 ^ S2) . i <= c by A9, A63, XXREAL_1:1;

ex DD being Division of CB st

( DD = T2 . i0 & ( for k being Element of NAT st k in dom DD holds

c < DD . k ) ) by A39;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A85, XXREAL_0:2; :: thesis: verum

end;then A84: i in dom S1 by A67, FINSEQ_3:25;

then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def 7;

then (S1 ^ S2) . i in rng S1 by A84, FUNCT_1:def 3;

then A85: (S1 ^ S2) . i <= c by A9, A63, XXREAL_1:1;

ex DD being Division of CB st

( DD = T2 . i0 & ( for k being Element of NAT st k in dom DD holds

c < DD . k ) ) by A39;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A85, XXREAL_0:2; :: thesis: verum

now :: thesis: ( j <= len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )

hence
(S1 ^ S2) . i < (S1 ^ S2) . j
by A70; :: thesis: verumassume A87:
j <= len S1
; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j

then i <= len S1 by A66, XXREAL_0:2;

then A88: ( j in dom S1 & i in dom S1 ) by A67, A87, FINSEQ_3:25;

then ( (S1 ^ S2) . j = S1 . j & (S1 ^ S2) . i = S1 . i ) by FINSEQ_1:def 7;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A66, A88, SEQM_3:def 1; :: thesis: verum

end;then i <= len S1 by A66, XXREAL_0:2;

then A88: ( j in dom S1 & i in dom S1 ) by A67, A87, FINSEQ_3:25;

then ( (S1 ^ S2) . j = S1 . j & (S1 ^ S2) . i = S1 . i ) by FINSEQ_1:def 7;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A66, A88, SEQM_3:def 1; :: thesis: verum

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 S

A93: for i being Element of NAT holds S

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

A112:
for i, k being Element of NAT
let i, k be Element of NAT ; :: thesis: 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; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) )

assume A96: S0 = T1 . i ; :: thesis: ( 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) ; :: thesis: 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;

end;divset ((T . i),k) = divset ((T1 . i),k)

let S0 be Division of AC; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) )

assume A96: S0 = T1 . i ; :: thesis: ( 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) ; :: thesis: 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 :: thesis: ( k <> 1 implies divset ((T . i),k) = divset ((T1 . i),k) )

assume A106:
k <> 1
; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: verum

now :: thesis: ( k = 1 implies divset ((T . i),k) = divset ((T1 . i),k) )

hence
divset ((T . i),k) = divset ((T1 . i),k)
by A104; :: thesis: verumassume A110:
k = 1
; :: thesis: 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 ;

:: thesis: verum

end;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 ;

:: thesis: verum

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

A134:
for i, k being Element of NAT
let i, k be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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) ; :: thesis: 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;

end;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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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) ; :: thesis: 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 :: thesis: ( k <> 1 implies divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) )

assume A125:
k <> 1
; :: thesis: 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 ;

:: thesis: verum

end;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 ;

:: thesis: verum

now :: thesis: ( k = 1 implies divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) )

hence
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
by A113, A115, A123; :: thesis: verum
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 ; :: thesis: 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 ;

:: thesis: verum

end;then A131: len S1 in dom S1 by FINSEQ_1:def 3;

assume A132: k = 1 ; :: thesis: 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 ;

:: thesis: verum

for S0 being Division of CB st S0 = T2 . i & k in Seg (len S0) holds

divset ((T2 . i),k) c= CB

proof

A139:
for i, k being Element of NAT
let i, k be Element of NAT ; :: thesis: for S0 being Division of CB st S0 = T2 . i & k in Seg (len S0) holds

divset ((T2 . i),k) c= CB

let S0 be Division of CB; :: thesis: ( S0 = T2 . i & k in Seg (len S0) implies divset ((T2 . i),k) c= CB )

assume A135: ( S0 = T2 . i & k in Seg (len S0) ) ; :: thesis: divset ((T2 . i),k) c= CB

then k in dom S0 by FINSEQ_1:def 3;

hence divset ((T2 . i),k) c= CB by A135, INTEGRA1:8; :: thesis: verum

end;divset ((T2 . i),k) c= CB

let S0 be Division of CB; :: thesis: ( S0 = T2 . i & k in Seg (len S0) implies divset ((T2 . i),k) c= CB )

assume A135: ( S0 = T2 . i & k in Seg (len S0) ) ; :: thesis: divset ((T2 . i),k) c= CB

then k in dom S0 by FINSEQ_1:def 3;

hence divset ((T2 . i),k) c= CB by A135, INTEGRA1:8; :: thesis: verum

for S0 being Division of AC st S0 = T1 . i & k in Seg (len S0) holds

divset ((T1 . i),k) c= AC

proof

defpred S
let i, k be Element of NAT ; :: thesis: for S0 being Division of AC st S0 = T1 . i & k in Seg (len S0) holds

divset ((T1 . i),k) c= AC

let S0 be Division of AC; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T1 . i),k) c= AC )

assume A140: ( S0 = T1 . i & k in Seg (len S0) ) ; :: thesis: divset ((T1 . i),k) c= AC

then k in dom S0 by FINSEQ_1:def 3;

hence divset ((T1 . i),k) c= AC by A140, INTEGRA1:8; :: thesis: verum

end;divset ((T1 . i),k) c= AC

let S0 be Division of AC; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T1 . i),k) c= AC )

assume A140: ( S0 = T1 . i & k in Seg (len S0) ) ; :: thesis: divset ((T1 . i),k) c= AC

then k in dom S0 by FINSEQ_1:def 3;

hence divset ((T1 . i),k) c= AC by A140, INTEGRA1:8; :: thesis: verum

( 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 S

proof

consider Sh1 being sequence of ( the carrier of X *) such that
let k be Element of NAT ; :: thesis: ex y being Element of the carrier of X * st S_{4}[k,y]

reconsider p1 = the middle_volume_Sequence of FAC,T1 . k as FinSequence of the carrier of X ;

reconsider p2 = the middle_volume_Sequence of FCB,T2 . k as FinSequence of X ;

p1 ^ p2 in the carrier of X * by FINSEQ_1:def 11;

hence ex p being Element of the carrier of X * st S_{4}[k,p]
; :: thesis: verum

end;reconsider p1 = the middle_volume_Sequence of FAC,T1 . k as FinSequence of the carrier of X ;

reconsider p2 = the middle_volume_Sequence of FCB,T2 . k as FinSequence of X ;

p1 ^ p2 in the carrier of X * by FINSEQ_1:def 11;

hence ex p being Element of the carrier of X * st S

B22: for x being Element of NAT holds S

now :: thesis: for k being Element of NAT holds Sh1 . k is middle_volume of FAB,T . k

then reconsider F = Sh1 as middle_volume_Sequence of FAB,T by INTEGR18:def 3;let k be Element of NAT ; :: thesis: Sh1 . k is middle_volume of FAB,T . k

consider 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 )

end;consider 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

hence
Sh1 . k is middle_volume of FAB,T . k
by B226, INTEGR18:def 1; :: thesis: verum
let i be Nat; :: thesis: ( 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) ; :: thesis: ex c being Point of X st

( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c )

end;( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c ) )

assume i in dom (T . k) ; :: thesis: 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;

end;

( n in dom S2 & i = (len S1) + n ) ) by U1, FINSEQ_1:25;

suppose VC1:
i in dom S1
; :: thesis: ex c being Point of X st

( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c )

( 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; :: thesis: verum

end;( 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; :: thesis: verum

suppose
ex n being Nat st

( n in dom S2 & i = (len S1) + n ) ; :: thesis: ex c being Point of X st

( c in rng (FAB | (divset ((T . k),i))) & (Sh1 . k) . i = (vol (divset ((T . k),i))) * c )

( n in dom S2 & i = (len S1) + n ) ; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: 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)

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;let i be Nat; :: thesis: (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 ; :: thesis: verum

end;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 ; :: thesis: verum

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 ;

A168: now :: thesis: for e being Real st 0 < e holds

ex m being Nat st

for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e

ex m being Nat st

for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e

let e be Real; :: thesis: ( 0 < e implies ex m being Nat st

for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e )

assume 0 < e ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e

then consider m being Nat such that

A169: for n being Nat st m <= n holds

|.(((delta PS2) . n) - 0).| < e by A25, SEQ_2:def 7;

take m = m; :: thesis: for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e

end;for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e )

assume 0 < e ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e

then consider m being Nat such that

A169: for n being Nat st m <= n holds

|.(((delta PS2) . n) - 0).| < e by A25, SEQ_2:def 7;

take m = m; :: thesis: for n being Nat st m <= n holds

|.(((delta S2) . n) - 0).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( m <= n implies |.(((delta S2) . n) - 0).| < e )

assume m <= n ; :: thesis: |.(((delta S2) . n) - 0).| < e

then |.(((delta PS2) . (n + 2)) - 0).| < e by A169, NAT_1:12;

then A171: |.((delta (PS2 . (n + 2))) - 0).| < e by INTEGRA3:def 2;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

ex k being Nat ex e1 being Division of CB st

( k = n1 & e1 = S2 . n1 & e1 = PS2 . (k + 2) ) by A29;

hence |.(((delta S2) . n) - 0).| < e by A171, INTEGRA3:def 2; :: thesis: verum

end;assume m <= n ; :: thesis: |.(((delta S2) . n) - 0).| < e

then |.(((delta PS2) . (n + 2)) - 0).| < e by A169, NAT_1:12;

then A171: |.((delta (PS2 . (n + 2))) - 0).| < e by INTEGRA3:def 2;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

ex k being Nat ex e1 being Division of CB st

( k = n1 & e1 = S2 . n1 & e1 = PS2 . (k + 2) ) by A29;

hence |.(((delta S2) . n) - 0).| < e by A171, INTEGRA3:def 2; :: thesis: verum

A172: now :: thesis: 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).| < e

then A215:
delta T2 is convergent
by SEQ_2:def 6;ex m being Nat st

for n being Nat st m <= n holds

|.(((delta T2) . n) - 0).| < e

let e be Real; :: thesis: ( 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 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.(((delta T2) . n) - 0).| < e

then 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; :: thesis: for n being Nat st m <= n holds

|.(((delta T2) . n) - 0).| < e

A175: e / 2 < e by A173, XREAL_1:216;

let n be Nat; :: thesis: ( m <= n implies |.(((delta T2) . n) - 0).| < e )

X1: n in NAT by ORDINAL1:def 12;

assume m <= n ; :: thesis: |.(((delta T2) . n) - 0).| < e

then |.(((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

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; :: thesis: verum

end;for n being Nat st m <= n holds

|.(((delta T2) . n) - 0).| < e )

assume A173: e > 0 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.(((delta T2) . n) - 0).| < e

then 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; :: thesis: for n being Nat st m <= n holds

|.(((delta T2) . n) - 0).| < e

A175: e / 2 < e by A173, XREAL_1:216;

let n be Nat; :: thesis: ( m <= n implies |.(((delta T2) . n) - 0).| < e )

X1: n in NAT by ORDINAL1:def 12;

assume m <= n ; :: thesis: |.(((delta T2) . n) - 0).| < e

then |.(((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

X1:
n in NAT
by ORDINAL1:def 12;
reconsider D = T2 . n as Division of CB ;

let y be Real; :: thesis: ( y in rng (upper_volume (XCB,(T2 . n))) implies y < e )

assume y in rng (upper_volume (XCB,(T2 . n))) ; :: thesis: 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;

end;let y be Real; :: thesis: ( y in rng (upper_volume (XCB,(T2 . n))) implies y < e )

assume y in rng (upper_volume (XCB,(T2 . n))) ; :: thesis: 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 :: thesis: ( i = 1 implies y < e )

assume A192:
i = 1
; :: thesis: y < e

then 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 ; :: thesis: verum

end;then 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 ; :: thesis: verum

now :: thesis: ( i <> 1 implies y < e )

hence
y < e
by A190; :: thesis: verumassume A210:
i <> 1
; :: thesis: y < e

then 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; :: thesis: verum

end;then 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; :: thesis: verum

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; :: thesis: verum

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 :: thesis: 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).| < e

then A253:
delta T is convergent
by SEQ_2:def 6;ex n being Nat st

for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e

let e be Real; :: thesis: ( 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 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e

then 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; :: thesis: for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e

let m be Nat; :: thesis: ( n <= m implies |.(((delta T) . m) - 0).| < e )

assume A222: n <= m ; :: thesis: |.(((delta T) . m) - 0).| < e

X1: 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

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; :: thesis: verum

end;for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e )

assume A219: 0 < e ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e

then 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; :: thesis: for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e

let m be Nat; :: thesis: ( n <= m implies |.(((delta T) . m) - 0).| < e )

assume A222: n <= m ; :: thesis: |.(((delta T) . m) - 0).| < e

X1: 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

max (rng (upper_volume (XAB,(T . m)))) in rng (upper_volume (XAB,(T . m)))
by XXREAL_2:def 8;
reconsider Tm = T . m as Division of AB ;

let y be Real; :: thesis: ( y in rng (upper_volume (XAB,(T . m))) implies y < e )

assume y in rng (upper_volume (XAB,(T . m))) ; :: thesis: 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;

end;let y be Real; :: thesis: ( y in rng (upper_volume (XAB,(T . m))) implies y < e )

assume y in rng (upper_volume (XAB,(T . m))) ; :: thesis: 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 )
;

end;

suppose
i <= len S1
; :: thesis: y < e

then 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; :: thesis: verum

end;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; :: thesis: verum

suppose
i > len S1
; :: thesis: y < e

then 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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum

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; :: thesis: verum