let a, b, c be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c holds

( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )

let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c implies ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) )

assume that

A1: a <= b and

A2: ['a,b'] c= dom f and

A3: f is_integrable_on ['a,b'] and

A4: f | ['a,b'] is bounded and

A5: c in ['a,b'] and

A6: b <> c ; :: thesis: ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )

A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A8: c <= b by A5, XXREAL_1:1;

then A9: ['c,b'] = [.c,b.] by INTEGRA5:def 3;

then A10: [.c,b.] = [.(lower_bound [.c,b.]),(upper_bound [.c,b.]).] by INTEGRA1:4;

then A11: upper_bound ['c,b'] = b by A9, INTEGRA1:5;

set FAB = f || ['a,b'];

set FAC = f || ['a,c'];

set FCB = f || ['c,b'];

A12: f || ['a,b'] is Function of ['a,b'],REAL by A2, Lm1;

A13: a <= c by A5, A7, XXREAL_1:1;

then A14: ['a,c'] = [.a,c.] by INTEGRA5:def 3;

then A15: [.a,c.] = [.(lower_bound [.a,c.]),(upper_bound [.a,c.]).] by INTEGRA1:4;

then A16: lower_bound ['a,c'] = a by A14, INTEGRA1:5;

A17: ['c,b'] c= ['a,b'] by A7, A13, A9, XXREAL_1:34;

then f | ['c,b'] is bounded by A4, RFUNCT_1:74;

then A18: (f || ['c,b']) | ['c,b'] is bounded ;

A19: lower_bound ['c,b'] = c by A9, A10, INTEGRA1:5;

ex PS2 being DivSequence of ['c,b'] st

( delta PS2 is convergent & lim (delta PS2) = 0 & ex K being Element of NAT st

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

A25: ( delta PS2 is convergent & lim (delta PS2) = 0 ) and

A26: ex K being Element of NAT st

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

consider K being Element of NAT such that

A27: for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

defpred S_{1}[ set , set ] means ex n being Element of NAT ex e being Division of ['c,b'] st

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

A28: for n being Element of NAT ex D being Element of divs ['c,b'] 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 ['c,b'] ;

defpred S_{2}[ Element of NAT , set ] means ex S being Division of ['c,b'] 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 ['c,b'] st

( D = T2 . n & ( for i being Element of NAT st i in dom D holds

c < D . i ) )

set XCB = chi (['c,b'],['c,b']);

consider T1 being DivSequence of ['a,c'] 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 ['c,b'] st

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

.= integral (f || ['c,b']) ;

A58: integral (f,a,c) = integral (f,['a,c']) by A13, INTEGRA5:def 4;

defpred S_{3}[ Element of NAT , set ] means ex S1 being Division of ['a,c'] ex S2 being Division of ['c,b'] st

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

A59: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by A7, INTEGRA1:4;

then A60: upper_bound ['a,b'] = b by A7, INTEGRA1:5;

A61: for i being Element of NAT ex T being Element of divs ['a,b'] st S_{3}[i,T]

A93: for i being Element of NAT holds S_{3}[i,T . i]
from FUNCT_2:sch 3(A61);

A94: lower_bound ['a,b'] = a by A7, A59, INTEGRA1:5;

A95: for i, k being Element of NAT

for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds

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

A112: for i, k being Element of NAT

for S01 being Division of ['a,c']

for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds

divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)

A134: for i, k being Element of NAT

for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds

divset ((T2 . i),k) c= ['c,b']

then f | ['a,c'] is bounded by A4, RFUNCT_1:74;

then A138: (f || ['a,c']) | ['a,c'] is bounded ;

A139: for i, k being Element of NAT

for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds

divset ((T1 . i),k) c= ['a,c']

A166: f || ['c,b'] is Function of ['c,b'],REAL by A2, A17, Lm1, XBOOLE_1:1;

then A167: lower_integral (f || ['c,b']) <= upper_integral (f || ['c,b']) by A18, INTEGRA1:49;

then A216: lim (delta T2) = 0 by A172, SEQ_2:def 7;

then A217: ( upper_sum ((f || ['c,b']),T2) is convergent & lim (upper_sum ((f || ['c,b']),T2)) = upper_integral (f || ['c,b']) ) by A166, A18, A215, INTEGRA4:9;

then A254: lim (delta T) = 0 by A218, SEQ_2:def 7;

(f || ['a,b']) | ['a,b'] is bounded by A4;

then A255: upper_integral (f || ['a,b']) = lim (upper_sum ((f || ['a,b']),T)) by A12, A253, A254, INTEGRA4:9;

A256: for i being Element of NAT holds lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i)))

A280: f || ['a,c'] is Function of ['a,c'],REAL by A2, A137, Lm1, XBOOLE_1:1;

then A281: ( f || ['a,c'] is upper_integrable & f || ['a,c'] is lower_integrable ) by A138, INTEGRA4:10;

A282: ( upper_sum ((f || ['a,c']),T1) is convergent & lim (upper_sum ((f || ['a,c']),T1)) = upper_integral (f || ['a,c']) ) by A280, A138, A53, INTEGRA4:9;

then A283: (upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b']) by A165, A217, A255, SEQ_2:6;

A284: ( lower_sum ((f || ['a,c']),T1) is convergent & lim (lower_sum ((f || ['a,c']),T1)) = lower_integral (f || ['a,c']) ) by A280, A138, A53, INTEGRA4:8;

(f || ['a,b']) | ['a,b'] is bounded by A4;

then A285: lower_integral (f || ['a,b']) = lim (lower_sum ((f || ['a,b']),T)) by A12, A253, A254, INTEGRA4:8;

( lower_sum ((f || ['c,b']),T2) is convergent & lim (lower_sum ((f || ['c,b']),T2)) = lower_integral (f || ['c,b']) ) by A166, A18, A215, A216, INTEGRA4:8;

then A286: (lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b']) by A279, A284, A285, SEQ_2:6;

integral (f,a,b) = integral (f,['a,b']) by A1, INTEGRA5:def 4

.= (integral (f || ['a,c'])) + (integral (f || ['c,b'])) by A165, A282, A217, A255, SEQ_2:6 ;

hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A58, A57; :: thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )

f || ['a,b'] is integrable by A3;

then A287: upper_integral (f || ['a,b']) = lower_integral (f || ['a,b']) ;

A288: ( f || ['c,b'] is upper_integrable & f || ['c,b'] is lower_integrable ) by A166, A18, INTEGRA4:10;

A289: lower_integral (f || ['a,c']) <= upper_integral (f || ['a,c']) by A280, A138, INTEGRA1:49;

then lower_integral (f || ['c,b']) = upper_integral (f || ['c,b']) by A287, A283, A286, A167, Th1;

then A290: f || ['c,b'] is integrable by A288;

lower_integral (f || ['a,c']) = upper_integral (f || ['a,c']) by A287, A283, A286, A289, A167, Th1;

then f || ['a,c'] is integrable by A281;

hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) by A290; :: thesis: verum

( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )

let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c implies ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) )

assume that

A1: a <= b and

A2: ['a,b'] c= dom f and

A3: f is_integrable_on ['a,b'] and

A4: f | ['a,b'] is bounded and

A5: c in ['a,b'] and

A6: b <> c ; :: thesis: ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )

A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A8: c <= b by A5, XXREAL_1:1;

then A9: ['c,b'] = [.c,b.] by INTEGRA5:def 3;

then A10: [.c,b.] = [.(lower_bound [.c,b.]),(upper_bound [.c,b.]).] by INTEGRA1:4;

then A11: upper_bound ['c,b'] = b by A9, INTEGRA1:5;

set FAB = f || ['a,b'];

set FAC = f || ['a,c'];

set FCB = f || ['c,b'];

A12: f || ['a,b'] is Function of ['a,b'],REAL by A2, Lm1;

A13: a <= c by A5, A7, XXREAL_1:1;

then A14: ['a,c'] = [.a,c.] by INTEGRA5:def 3;

then A15: [.a,c.] = [.(lower_bound [.a,c.]),(upper_bound [.a,c.]).] by INTEGRA1:4;

then A16: lower_bound ['a,c'] = a by A14, INTEGRA1:5;

A17: ['c,b'] c= ['a,b'] by A7, A13, A9, XXREAL_1:34;

then f | ['c,b'] is bounded by A4, RFUNCT_1:74;

then A18: (f || ['c,b']) | ['c,b'] is bounded ;

A19: lower_bound ['c,b'] = c by A9, A10, INTEGRA1:5;

ex PS2 being DivSequence of ['c,b'] st

( delta PS2 is convergent & lim (delta PS2) = 0 & ex K being Element of NAT st

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

proof

then consider PS2 being DivSequence of ['c,b'] such that
c < b
by A6, A8, XXREAL_0:1;

then vol ['c,b'] > 0 by A19, A11, XREAL_1:50;

then consider T being DivSequence of ['c,b'] such that

A20: ( delta T is convergent & lim (delta T) = 0 ) and

A21: for n being Element of NAT ex Tn being Division of ['c,b'] st

( Tn divide_into_equal n + 1 & T . n = Tn ) by Th16;

take T ; :: thesis: ( delta T is convergent & lim (delta T) = 0 & ex K being Element of NAT st

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

( S2i = T . i & 2 <= len S2i ) ) by A20; :: thesis: verum

end;then vol ['c,b'] > 0 by A19, A11, XREAL_1:50;

then consider T being DivSequence of ['c,b'] such that

A20: ( delta T is convergent & lim (delta T) = 0 ) and

A21: for n being Element of NAT ex Tn being Division of ['c,b'] st

( Tn divide_into_equal n + 1 & T . n = Tn ) by Th16;

take T ; :: thesis: ( delta T is convergent & lim (delta T) = 0 & ex K being Element of NAT st

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

now :: thesis: for i being Element of NAT st 2 <= i holds

ex Tn being Division of ['c,b'] st

( Tn = T . i & 2 <= len Tn )

hence
( delta T is convergent & lim (delta T) = 0 & ex K being Element of NAT st ex Tn being Division of ['c,b'] st

( Tn = T . i & 2 <= len Tn )

let i be Element of NAT ; :: thesis: ( 2 <= i implies ex Tn being Division of ['c,b'] st

( Tn = T . i & 2 <= len Tn ) )

assume A22: 2 <= i ; :: thesis: ex Tn being Division of ['c,b'] st

( Tn = T . i & 2 <= len Tn )

consider Tn being Division of ['c,b'] such that

A23: Tn divide_into_equal i + 1 and

A24: T . i = Tn by A21;

reconsider Tn = Tn as Division of ['c,b'] ;

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

thus Tn = T . i by A24; :: thesis: 2 <= len Tn

len Tn = i + 1 by A23, INTEGRA4:def 1;

then i <= len Tn by NAT_1:11;

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

end;( Tn = T . i & 2 <= len Tn ) )

assume A22: 2 <= i ; :: thesis: ex Tn being Division of ['c,b'] st

( Tn = T . i & 2 <= len Tn )

consider Tn being Division of ['c,b'] such that

A23: Tn divide_into_equal i + 1 and

A24: T . i = Tn by A21;

reconsider Tn = Tn as Division of ['c,b'] ;

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

thus Tn = T . i by A24; :: thesis: 2 <= len Tn

len Tn = i + 1 by A23, INTEGRA4:def 1;

then i <= len Tn by NAT_1:11;

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

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

( S2i = T . i & 2 <= len S2i ) ) by A20; :: thesis: verum

A25: ( delta PS2 is convergent & lim (delta PS2) = 0 ) and

A26: ex K being Element of NAT st

for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

consider K being Element of NAT such that

A27: for i being Element of NAT st K <= i holds

ex S2i being Division of ['c,b'] st

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

defpred S

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

A28: for n being Element of NAT ex D being Element of divs ['c,b'] st S

proof

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

reconsider D = PS2 . (n + K) as Element of divs ['c,b'] by INTEGRA1:def 3;

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

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

end;reconsider D = PS2 . (n + K) as Element of divs ['c,b'] 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 ['c,b'] ;

defpred S

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

A30: now :: thesis: for i being Element of NAT ex S2i being Division of ['c,b'] st

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

A31:
for i being Element of NAT ex T being Element of divs ['c,b'] st S( S2i = S2 . i & 2 <= len S2i )

let i be Element of NAT ; :: thesis: ex S2i being Division of ['c,b'] st

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

ex n being Element of NAT ex e being Division of ['c,b'] st

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

hence ex S2i being Division of ['c,b'] st

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

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

ex n being Element of NAT ex e being Division of ['c,b'] st

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

hence ex S2i being Division of ['c,b'] st

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

proof

consider T2 being DivSequence of ['c,b'] such that
let i be Element of NAT ; :: thesis: ex T being Element of divs ['c,b'] st S_{2}[i,T]

consider S being Division of ['c,b'] such that

A32: S = S2 . i and

A33: 2 <= len S by A30;

set T = S /^ 1;

A34: 1 <= len S by A33, XXREAL_0:2;

2 - 1 <= (len S) - 1 by A33, XREAL_1:13;

then A35: 1 <= len (S /^ 1) by A34, RFINSEQ:def 1;

then len (S /^ 1) in Seg (len (S /^ 1)) ;

then len (S /^ 1) in dom (S /^ 1) by FINSEQ_1:def 3;

then (S /^ 1) . (len (S /^ 1)) = S . ((len (S /^ 1)) + 1) by A34, RFINSEQ:def 1;

then (S /^ 1) . (len (S /^ 1)) = S . (((len S) - 1) + 1) by A34, RFINSEQ:def 1;

then A36: (S /^ 1) . (len (S /^ 1)) = upper_bound ['c,b'] by INTEGRA1:def 2;

( rng S c= ['c,b'] & rng (S /^ 1) c= rng S ) by FINSEQ_5:33, INTEGRA1:def 2;

then A37: rng (S /^ 1) c= ['c,b'] ;

( not S /^ 1 is empty & S /^ 1 is increasing ) by A33, A35, INTEGRA1:34, XXREAL_0:2;

then S /^ 1 is Division of ['c,b'] by A37, A36, INTEGRA1:def 2;

then S /^ 1 is Element of divs ['c,b'] by INTEGRA1:def 3;

hence ex T being Element of divs ['c,b'] st S_{2}[i,T]
by A32; :: thesis: verum

end;consider S being Division of ['c,b'] such that

A32: S = S2 . i and

A33: 2 <= len S by A30;

set T = S /^ 1;

A34: 1 <= len S by A33, XXREAL_0:2;

2 - 1 <= (len S) - 1 by A33, XREAL_1:13;

then A35: 1 <= len (S /^ 1) by A34, RFINSEQ:def 1;

then len (S /^ 1) in Seg (len (S /^ 1)) ;

then len (S /^ 1) in dom (S /^ 1) by FINSEQ_1:def 3;

then (S /^ 1) . (len (S /^ 1)) = S . ((len (S /^ 1)) + 1) by A34, RFINSEQ:def 1;

then (S /^ 1) . (len (S /^ 1)) = S . (((len S) - 1) + 1) by A34, RFINSEQ:def 1;

then A36: (S /^ 1) . (len (S /^ 1)) = upper_bound ['c,b'] by INTEGRA1:def 2;

( rng S c= ['c,b'] & rng (S /^ 1) c= rng S ) by FINSEQ_5:33, INTEGRA1:def 2;

then A37: rng (S /^ 1) c= ['c,b'] ;

( not S /^ 1 is empty & S /^ 1 is increasing ) by A33, A35, INTEGRA1:34, XXREAL_0:2;

then S /^ 1 is Division of ['c,b'] by A37, A36, INTEGRA1:def 2;

then S /^ 1 is Element of divs ['c,b'] by INTEGRA1:def 3;

hence ex T being Element of divs ['c,b'] st S

A38: for i being Element of NAT holds S

A39: for n being Element of NAT ex D being Division of ['c,b'] st

( D = T2 . n & ( for i being Element of NAT st i in dom D holds

c < D . i ) )

proof

set XAC = chi (['a,c'],['a,c']);
let n be Element of NAT ; :: thesis: ex D being Division of ['c,b'] 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 ['c,b'] ;

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 ['c,b'] such that

A40: E = S2 . n and

A41: T2 . n = E /^ 1 by A38;

A42: ex E1 being Division of ['c,b'] 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 1 in Seg (len E) ;

then A45: 1 in dom E by FINSEQ_1:def 3;

then ( rng E c= ['c,b'] & 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 Seg (len E) by A40, A42;

then 2 in dom E by FINSEQ_1:def 3;

then A47: E . 1 < E . 2 by A45, SEQM_3:def 1;

len D = (len E) - 1 by A41, A44, RFINSEQ:def 1;

then 1 in Seg (len D) by A43;

then A48: 1 in dom D by FINSEQ_1:def 3;

then A49: D . 1 = E . (1 + 1) by A41, 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 ['c,b'] ;

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 ['c,b'] such that

A40: E = S2 . n and

A41: T2 . n = E /^ 1 by A38;

A42: ex E1 being Division of ['c,b'] 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 1 in Seg (len E) ;

then A45: 1 in dom E by FINSEQ_1:def 3;

then ( rng E c= ['c,b'] & 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 Seg (len E) by A40, A42;

then 2 in dom E by FINSEQ_1:def 3;

then A47: E . 1 < E . 2 by A45, SEQM_3:def 1;

len D = (len E) - 1 by A41, A44, RFINSEQ:def 1;

then 1 in Seg (len D) by A43;

then A48: 1 in dom D by FINSEQ_1:def 3;

then A49: D . 1 = E . (1 + 1) by A41, 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

set XCB = chi (['c,b'],['c,b']);

consider T1 being DivSequence of ['a,c'] 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 ['c,b'] st

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

proof

A57: integral (f,c,b) =
integral (f,['c,b'])
by A8, INTEGRA5:def 4
let n be Element of NAT ; :: thesis: ex D being Division of ['c,b'] st

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

reconsider D = T2 . n as Division of ['c,b'] ;

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

consider E being Division of ['c,b'] such that

A55: E = S2 . n and

A56: T2 . n = E /^ 1 by A38;

ex E1 being Division of ['c,b'] 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 A56, RFINSEQ:def 1; :: thesis: verum

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

reconsider D = T2 . n as Division of ['c,b'] ;

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

consider E being Division of ['c,b'] such that

A55: E = S2 . n and

A56: T2 . n = E /^ 1 by A38;

ex E1 being Division of ['c,b'] 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 A56, RFINSEQ:def 1; :: thesis: verum

.= integral (f || ['c,b']) ;

A58: integral (f,a,c) = integral (f,['a,c']) by A13, INTEGRA5:def 4;

defpred S

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

A59: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by A7, INTEGRA1:4;

then A60: upper_bound ['a,b'] = b by A7, INTEGRA1:5;

A61: for i being Element of NAT ex T being Element of divs ['a,b'] st S

proof

consider T being DivSequence of ['a,b'] such that
let i0 be Element of NAT ; :: thesis: ex T being Element of divs ['a,b'] st S_{3}[i0,T]

reconsider S1 = T1 . i0 as Division of ['a,c'] ;

reconsider S2 = T2 . i0 as Division of ['c,b'] ;

set T = S1 ^ S2;

ex D being Division of ['c,b'] 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= ['a,c'] by INTEGRA1:def 2;

rng S2 c= ['c,b'] by INTEGRA1:def 2;

then (rng S1) \/ (rng S2) c= ['a,c'] \/ ['c,b'] by A63, XBOOLE_1:13;

then (rng S1) \/ (rng S2) c= [.a,b.] by A13, A8, A14, A9, XXREAL_1:174;

then A92: rng (S1 ^ S2) c= ['a,b'] by A7, FINSEQ_1:31;

(S1 ^ S2) . (len (S1 ^ S2)) = (S1 ^ S2) . ((len S1) + (len S2)) by FINSEQ_1:22

.= S2 . (len S2) by A62, FINSEQ_1:def 7

.= upper_bound ['a,b'] by A60, A11, INTEGRA1:def 2 ;

then S1 ^ S2 is Division of ['a,b'] by A92, A91, INTEGRA1:def 2;

then S1 ^ S2 is Element of divs ['a,b'] by INTEGRA1:def 3;

hence ex T being Element of divs ['a,b'] st S_{3}[i0,T]
; :: thesis: verum

end;reconsider S1 = T1 . i0 as Division of ['a,c'] ;

reconsider S2 = T2 . i0 as Division of ['c,b'] ;

set T = S1 ^ S2;

ex D being Division of ['c,b'] 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= ['a,c'] 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 A91:
S1 ^ S2 is 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) and

A65: j in dom (S1 ^ S2) and

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

A67: 1 <= i by A64, FINSEQ_3:25;

A68: j <= len (S1 ^ S2) by A65, FINSEQ_3:25;

A69: i <= len (S1 ^ S2) by A64, FINSEQ_3:25;

end;assume that

A64: i in dom (S1 ^ S2) and

A65: j in dom (S1 ^ S2) and

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

A67: 1 <= i by A64, FINSEQ_3:25;

A68: j <= len (S1 ^ S2) by A65, FINSEQ_3:25;

A69: i <= len (S1 ^ S2) by A64, FINSEQ_3:25;

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

A86:
1 <= j
by A65, FINSEQ_3:25;
j <= (len S1) + (len S2)
by A68, FINSEQ_1:22;

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

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

then A73: (S1 ^ S2) . j = S2 . (j - (len S1)) by A68, 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;

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

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

then 1 <= 1 + m by A74, XREAL_1:19;

then 1 + m in Seg (len S2) by A75, A71;

then A76: j - (len S1) in dom S2 by A75, FINSEQ_1:def 3;

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

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

then A73: (S1 ^ S2) . j = S2 . (j - (len S1)) by A68, 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;

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

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

then 1 <= 1 + m by A74, XREAL_1:19;

then 1 + m in Seg (len S2) by A75, A71;

then A76: j - (len S1) in dom S2 by A75, FINSEQ_1:def 3;

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

i <= (len S1) + (len S2)
by A69, FINSEQ_1:22;

then A78: i - (len S1) <= len S2 by XREAL_1:20;

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

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;

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

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

then 1 <= 1 + m by A81, XREAL_1:19;

then 1 + m in Seg (len S2) by A82, A78;

then A83: i - (len S1) in dom S2 by A82, FINSEQ_1:def 3;

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

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

end;then A78: i - (len S1) <= len S2 by XREAL_1:20;

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

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;

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

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

then 1 <= 1 + m by A81, XREAL_1:19;

then 1 + m in Seg (len S2) by A82, A78;

then A83: i - (len S1) in dom S2 by A82, FINSEQ_1:def 3;

(S1 ^ S2) . i = S2 . (i - (len S1)) by A69, 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 A14, A63, XXREAL_1:1;

ex DD being Division of ['c,b'] 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 A14, A63, XXREAL_1:1;

ex DD being Division of ['c,b'] 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 A88: j in dom S1 by A86, FINSEQ_3:25;

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

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

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

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

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

end;then A88: j in dom S1 by A86, FINSEQ_3:25;

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

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

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

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

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

rng S2 c= ['c,b'] by INTEGRA1:def 2;

then (rng S1) \/ (rng S2) c= ['a,c'] \/ ['c,b'] by A63, XBOOLE_1:13;

then (rng S1) \/ (rng S2) c= [.a,b.] by A13, A8, A14, A9, XXREAL_1:174;

then A92: rng (S1 ^ S2) c= ['a,b'] by A7, FINSEQ_1:31;

(S1 ^ S2) . (len (S1 ^ S2)) = (S1 ^ S2) . ((len S1) + (len S2)) by FINSEQ_1:22

.= S2 . (len S2) by A62, FINSEQ_1:def 7

.= upper_bound ['a,b'] by A60, A11, INTEGRA1:def 2 ;

then S1 ^ S2 is Division of ['a,b'] by A92, A91, INTEGRA1:def 2;

then S1 ^ S2 is Element of divs ['a,b'] by INTEGRA1:def 3;

hence ex T being Element of divs ['a,b'] st S

A93: for i being Element of NAT holds S

A94: lower_bound ['a,b'] = a by A7, A59, INTEGRA1:5;

A95: for i, k being Element of NAT

for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds

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

proof

A111:
upper_bound ['a,c'] = c
by A14, A15, INTEGRA1:5;
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds

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

let S0 be Division of ['a,c']; :: 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 ['a,b'] ;

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 ['a,c'], S2 being Division of ['c,b'] such that

A98: S1 = T1 . i and

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;

len S = (len S1) + (len S2) by A99, FINSEQ_1:22;

then len S1 <= len S by NAT_1:11;

then Seg (len S1) c= Seg (len S) by FINSEQ_1:5;

then k in Seg (len S) by A96, A100, A98;

then A102: k in dom S by FINSEQ_1:def 3;

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 ['a,c']; :: 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 ['a,b'] ;

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 ['a,c'], S2 being Division of ['c,b'] such that

A98: S1 = T1 . i and

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;

len S = (len S1) + (len S2) by A99, FINSEQ_1:22;

then len S1 <= len S by NAT_1:11;

then Seg (len S1) c= Seg (len S) by FINSEQ_1:5;

then k in Seg (len S) by A96, A100, A98;

then A102: k in dom S by FINSEQ_1:def 3;

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

( k <= len S1 & k - 1 <= k - 0 )
by A96, A100, A98, FINSEQ_1:1, XREAL_1:10;

then A105: k - 1 <= len S1 by XXREAL_0:2;

assume A106: k <> 1 ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)

1 <= k by A100, FINSEQ_1:1;

then A107: 1 < k by A106, XXREAL_0:1;

then 1 + 1 <= k by NAT_1:13;

then A108: 2 - 1 <= k - 1 by XREAL_1:9;

k - 1 is Element of NAT by A107, NAT_1:20;

then k - 1 in Seg (len S1) by A105, A108;

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;then A105: k - 1 <= len S1 by XXREAL_0:2;

assume A106: k <> 1 ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)

1 <= k by A100, FINSEQ_1:1;

then A107: 1 < k by A106, XXREAL_0:1;

then 1 + 1 <= k by NAT_1:13;

then A108: 2 - 1 <= k - 1 by XREAL_1:9;

k - 1 is Element of NAT by A107, NAT_1:20;

then k - 1 in Seg (len S1) by A105, A108;

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 ['a,b']),(upper_bound (divset ((T . i),k))).] by A102, A103, INTEGRA1:def 4

.= [.(lower_bound ['a,b']),(S . k).] by A102, A110, INTEGRA1:def 4

.= [.(lower_bound ['a,b']),(S1 . k).] by A99, A101, FINSEQ_1:def 7

.= [.(lower_bound (divset ((T1 . i),k))),(S1 . 1).] by A94, A16, 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 ['a,b']),(upper_bound (divset ((T . i),k))).] by A102, A103, INTEGRA1:def 4

.= [.(lower_bound ['a,b']),(S . k).] by A102, A110, INTEGRA1:def 4

.= [.(lower_bound ['a,b']),(S1 . k).] by A99, A101, FINSEQ_1:def 7

.= [.(lower_bound (divset ((T1 . i),k))),(S1 . 1).] by A94, A16, A98, A101, A110, INTEGRA1:def 4

.= divset ((T1 . i),k) by A98, A101, A97, A110, INTEGRA1:def 4 ;

:: thesis: verum

A112: for i, k being Element of NAT

for S01 being Division of ['a,c']

for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds

divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)

proof

set XAB = chi (['a,b'],['a,b']);
let i, k be Element of NAT ; :: thesis: for S01 being Division of ['a,c']

for S02 being Division of ['c,b'] 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 ['a,c']; :: thesis: for S02 being Division of ['c,b'] 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 ['c,b']; :: thesis: ( S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) implies divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )

assume that

A113: S01 = T1 . i and

A114: 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 ['a,b'] ;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A115: S1 = T1 . i and

A116: 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 A114, A116, 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 ['c,b'] 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 ['a,c']; :: thesis: for S02 being Division of ['c,b'] 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 ['c,b']; :: thesis: ( S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) implies divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )

assume that

A113: S01 = T1 . i and

A114: 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 ['a,b'] ;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A115: S1 = T1 . i and

A116: 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 A114, A116, 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) )

( k <= len S2 & k - 1 <= k - 0 )
by A114, A118, A116, FINSEQ_1:1, XREAL_1:10;

then A124: k - 1 <= len S2 by XXREAL_0:2;

assume A125: k <> 1 ; :: thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)

A126: 1 <= k by A118, FINSEQ_1:1;

then A127: 1 < k by A125, XXREAL_0:1;

then 1 + 1 <= k by NAT_1:13;

then A128: 2 - 1 <= k - 1 by XREAL_1:9;

k - 1 is Element of NAT by A127, NAT_1:20;

then k - 1 in Seg (len S2) by A124, A128;

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 A116, A119, A125, INTEGRA1:def 4

.= divset ((T2 . i),k) by A116, A119, A121, A125, INTEGRA1:def 4 ;

:: thesis: verum

end;then A124: k - 1 <= len S2 by XXREAL_0:2;

assume A125: k <> 1 ; :: thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)

A126: 1 <= k by A118, FINSEQ_1:1;

then A127: 1 < k by A125, XXREAL_0:1;

then 1 + 1 <= k by NAT_1:13;

then A128: 2 - 1 <= k - 1 by XREAL_1:9;

k - 1 is Element of NAT by A127, NAT_1:20;

then k - 1 in Seg (len S2) by A124, A128;

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 A116, A119, A125, INTEGRA1:def 4

.= divset ((T2 . i),k) by A116, 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 ['a,c']),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:def 2

.= [.(lower_bound ['c,b']),(S . ((len S1) + k)).] by A19, A111, A120, A133, INTEGRA1:def 4

.= [.(lower_bound ['c,b']),(S2 . k).] by A117, A119, FINSEQ_1:def 7

.= [.(lower_bound (divset ((T2 . i),k))),(S2 . 1).] by A116, A119, A132, INTEGRA1:def 4

.= divset ((T2 . i),k) by A116, 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 ['a,c']),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:def 2

.= [.(lower_bound ['c,b']),(S . ((len S1) + k)).] by A19, A111, A120, A133, INTEGRA1:def 4

.= [.(lower_bound ['c,b']),(S2 . k).] by A117, A119, FINSEQ_1:def 7

.= [.(lower_bound (divset ((T2 . i),k))),(S2 . 1).] by A116, A119, A132, INTEGRA1:def 4

.= divset ((T2 . i),k) by A116, A119, A121, A132, INTEGRA1:def 4 ;

:: thesis: verum

A134: for i, k being Element of NAT

for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds

divset ((T2 . i),k) c= ['c,b']

proof

A137:
['a,c'] c= ['a,b']
by A7, A8, A14, XXREAL_1:34;
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds

divset ((T2 . i),k) c= ['c,b']

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

assume that

A135: S0 = T2 . i and

A136: k in Seg (len S0) ; :: thesis: divset ((T2 . i),k) c= ['c,b']

k in dom S0 by A136, FINSEQ_1:def 3;

hence divset ((T2 . i),k) c= ['c,b'] by A135, INTEGRA1:8; :: thesis: verum

end;divset ((T2 . i),k) c= ['c,b']

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

assume that

A135: S0 = T2 . i and

A136: k in Seg (len S0) ; :: thesis: divset ((T2 . i),k) c= ['c,b']

k in dom S0 by A136, FINSEQ_1:def 3;

hence divset ((T2 . i),k) c= ['c,b'] by A135, INTEGRA1:8; :: thesis: verum

then f | ['a,c'] is bounded by A4, RFUNCT_1:74;

then A138: (f || ['a,c']) | ['a,c'] is bounded ;

A139: for i, k being Element of NAT

for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds

divset ((T1 . i),k) c= ['a,c']

proof

A142:
for i being Element of NAT holds upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i)))
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds

divset ((T1 . i),k) c= ['a,c']

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

assume that

A140: S0 = T1 . i and

A141: k in Seg (len S0) ; :: thesis: divset ((T1 . i),k) c= ['a,c']

k in dom S0 by A141, FINSEQ_1:def 3;

hence divset ((T1 . i),k) c= ['a,c'] by A140, INTEGRA1:8; :: thesis: verum

end;divset ((T1 . i),k) c= ['a,c']

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

assume that

A140: S0 = T1 . i and

A141: k in Seg (len S0) ; :: thesis: divset ((T1 . i),k) c= ['a,c']

k in dom S0 by A141, FINSEQ_1:def 3;

hence divset ((T1 . i),k) c= ['a,c'] by A140, INTEGRA1:8; :: thesis: verum

proof

A164:
for i being Element of NAT holds Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i))))
let i be Element of NAT ; :: thesis: upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i)))

reconsider F = upper_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;

reconsider F1 = upper_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;

reconsider F2 = upper_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;

reconsider S = T . i as Division of ['a,b'] ;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A143: S1 = T1 . i and

A144: S2 = T2 . i and

A145: T . i = S1 ^ S2 by A93;

A146: len F = len S by INTEGRA1:def 6

.= (len S1) + (len S2) by A145, FINSEQ_1:22

.= (len F1) + (len S2) by A143, INTEGRA1:def 6

.= (len F1) + (len F2) by A144, INTEGRA1:def 6 ;

hence upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A157, A147, FINSEQ_1:def 7; :: thesis: verum

end;reconsider F = upper_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;

reconsider F1 = upper_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;

reconsider F2 = upper_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;

reconsider S = T . i as Division of ['a,b'] ;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A143: S1 = T1 . i and

A144: S2 = T2 . i and

A145: T . i = S1 ^ S2 by A93;

A146: len F = len S by INTEGRA1:def 6

.= (len S1) + (len S2) by A145, FINSEQ_1:22

.= (len F1) + (len S2) by A143, INTEGRA1:def 6

.= (len F1) + (len F2) by A144, INTEGRA1:def 6 ;

A147: now :: thesis: for k being Nat st k in dom F2 holds

F . ((len F1) + k) = F2 . k

F . ((len F1) + k) = F2 . k

let k be Nat; :: thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )

assume A148: k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k

then A149: k in Seg (len F2) by FINSEQ_1:def 3;

then 1 <= k by FINSEQ_1:1;

then A150: 1 + (len F1) <= k + (len F1) by XREAL_1:6;

k <= len F2 by A149, FINSEQ_1:1;

then A151: (len F1) + k <= len F by A146, XREAL_1:6;

1 <= 1 + (len F1) by NAT_1:11;

then 1 <= k + (len F1) by A150, XXREAL_0:2;

then k + (len F1) in Seg (len F) by A151;

then (len F1) + k in Seg (len S) by INTEGRA1:def 6;

then (len F1) + k in dom S by FINSEQ_1:def 3;

then A152: F . ((len F1) + k) = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 6;

k in Seg (len F2) by A148, FINSEQ_1:def 3;

then A153: k in Seg (len S2) by A144, INTEGRA1:def 6;

then A154: k in dom S2 by FINSEQ_1:def 3;

len F1 = len S1 by A143, INTEGRA1:def 6;

then A155: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A143, A144, A153;

then A156: divset ((T . i),((len F1) + k)) c= ['c,b'] by A134, A144, A153;

then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17;

then F . ((len F1) + k) = (upper_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A152, A155, A156, Th3;

hence F . ((len F1) + k) = F2 . k by A144, A154, INTEGRA1:def 6; :: thesis: verum

end;assume A148: k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k

then A149: k in Seg (len F2) by FINSEQ_1:def 3;

then 1 <= k by FINSEQ_1:1;

then A150: 1 + (len F1) <= k + (len F1) by XREAL_1:6;

k <= len F2 by A149, FINSEQ_1:1;

then A151: (len F1) + k <= len F by A146, XREAL_1:6;

1 <= 1 + (len F1) by NAT_1:11;

then 1 <= k + (len F1) by A150, XXREAL_0:2;

then k + (len F1) in Seg (len F) by A151;

then (len F1) + k in Seg (len S) by INTEGRA1:def 6;

then (len F1) + k in dom S by FINSEQ_1:def 3;

then A152: F . ((len F1) + k) = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 6;

k in Seg (len F2) by A148, FINSEQ_1:def 3;

then A153: k in Seg (len S2) by A144, INTEGRA1:def 6;

then A154: k in dom S2 by FINSEQ_1:def 3;

len F1 = len S1 by A143, INTEGRA1:def 6;

then A155: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A143, A144, A153;

then A156: divset ((T . i),((len F1) + k)) c= ['c,b'] by A134, A144, A153;

then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17;

then F . ((len F1) + k) = (upper_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A152, A155, A156, Th3;

hence F . ((len F1) + k) = F2 . k by A144, A154, INTEGRA1:def 6; :: thesis: verum

A157: now :: thesis: for k being Nat st k in dom F1 holds

F . k = F1 . k

dom F = Seg ((len F1) + (len F2))
by A146, FINSEQ_1:def 3;F . k = F1 . k

let k be Nat; :: thesis: ( k in dom F1 implies F . k = F1 . k )

assume k in dom F1 ; :: thesis: F . k = F1 . k

then A158: k in Seg (len F1) by FINSEQ_1:def 3;

then A159: k in Seg (len S1) by A143, INTEGRA1:def 6;

then A160: k in dom S1 by FINSEQ_1:def 3;

len F1 <= len F by A146, NAT_1:11;

then Seg (len F1) c= Seg (len F) by FINSEQ_1:5;

then k in Seg (len F) by A158;

then k in Seg (len S) by INTEGRA1:def 6;

then k in dom S by FINSEQ_1:def 3;

then A161: F . k = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by INTEGRA1:def 6;

A162: divset ((T . i),k) = divset ((T1 . i),k) by A95, A143, A159;

then A163: divset ((T . i),k) c= ['a,c'] by A139, A143, A159;

then divset ((T . i),k) c= ['a,b'] by A137;

then F . k = (upper_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A161, A162, A163, Th3;

hence F . k = F1 . k by A143, A160, INTEGRA1:def 6; :: thesis: verum

end;assume k in dom F1 ; :: thesis: F . k = F1 . k

then A158: k in Seg (len F1) by FINSEQ_1:def 3;

then A159: k in Seg (len S1) by A143, INTEGRA1:def 6;

then A160: k in dom S1 by FINSEQ_1:def 3;

len F1 <= len F by A146, NAT_1:11;

then Seg (len F1) c= Seg (len F) by FINSEQ_1:5;

then k in Seg (len F) by A158;

then k in Seg (len S) by INTEGRA1:def 6;

then k in dom S by FINSEQ_1:def 3;

then A161: F . k = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by INTEGRA1:def 6;

A162: divset ((T . i),k) = divset ((T1 . i),k) by A95, A143, A159;

then A163: divset ((T . i),k) c= ['a,c'] by A139, A143, A159;

then divset ((T . i),k) c= ['a,b'] by A137;

then F . k = (upper_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A161, A162, A163, Th3;

hence F . k = F1 . k by A143, A160, INTEGRA1:def 6; :: thesis: verum

hence upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A157, A147, FINSEQ_1:def 7; :: thesis: verum

proof

let i be Element of NAT ; :: thesis: Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i))))

upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A142;

hence Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum

end;upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A142;

hence Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum

now :: thesis: for i being Nat holds (upper_sum ((f || ['a,b']),T)) . i = ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i)

then A165:
upper_sum ((f || ['a,b']),T) = (upper_sum ((f || ['a,c']),T1)) + (upper_sum ((f || ['c,b']),T2))
by SEQ_1:7;let i be Nat; :: thesis: (upper_sum ((f || ['a,b']),T)) . i = ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i)

reconsider ii = i as Element of NAT by ORDINAL1:def 12;

thus (upper_sum ((f || ['a,b']),T)) . i = upper_sum ((f || ['a,b']),(T . ii)) by INTEGRA2:def 2

.= (upper_sum ((f || ['a,c']),(T1 . ii))) + (Sum (upper_volume ((f || ['c,b']),(T2 . ii)))) by A164

.= ((upper_sum ((f || ['a,c']),T1)) . i) + (upper_sum ((f || ['c,b']),(T2 . ii))) by INTEGRA2:def 2

.= ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def 2 ; :: thesis: verum

end;reconsider ii = i as Element of NAT by ORDINAL1:def 12;

thus (upper_sum ((f || ['a,b']),T)) . i = upper_sum ((f || ['a,b']),(T . ii)) by INTEGRA2:def 2

.= (upper_sum ((f || ['a,c']),(T1 . ii))) + (Sum (upper_volume ((f || ['c,b']),(T2 . ii)))) by A164

.= ((upper_sum ((f || ['a,c']),T1)) . i) + (upper_sum ((f || ['c,b']),(T2 . ii))) by INTEGRA2:def 2

.= ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def 2 ; :: thesis: verum

A166: f || ['c,b'] is Function of ['c,b'],REAL by A2, A17, Lm1, XBOOLE_1:1;

then A167: lower_integral (f || ['c,b']) <= upper_integral (f || ['c,b']) by A18, INTEGRA1:49;

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 )

A170: n <= n + K by NAT_1:11;

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

then m <= n + K by A170, XXREAL_0:2;

then |.(((delta PS2) . (n + K)) - 0).| < e by A169;

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

n in NAT by ORDINAL1:def 12;

then ex k being Element of NAT ex e1 being Division of ['c,b'] st

( k = n & e1 = S2 . n & e1 = PS2 . (k + K) ) by A29;

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

end;A170: n <= n + K by NAT_1:11;

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

then m <= n + K by A170, XXREAL_0:2;

then |.(((delta PS2) . (n + K)) - 0).| < e by A169;

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

n in NAT by ORDINAL1:def 12;

then ex k being Element of NAT ex e1 being Division of ['c,b'] st

( k = n & e1 = S2 . n & e1 = PS2 . (k + K) ) 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 nn being Nat st m <= nn holds

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

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

for nn being Nat st m <= nn holds

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

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

for nn being Nat st m <= nn holds

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

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

for nn being Nat st m <= nn holds

|.(((delta T2) . nn) - 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 nn being Nat st m <= nn holds

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

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

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

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

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

|.(((delta S2) . n) - 0).| < e / 2 by A174, A176;

then ( 0 <= delta (S2 . n) & |.(delta (S2 . n)).| < e / 2 ) by INTEGRA3:9, INTEGRA3:def 2;

then A177: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) < e / 2 by ABSVALUE:def 1;

A178: for y being Real st y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) holds

y < e

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) . nn) - 0).| < e by INTEGRA3:def 2; :: thesis: verum

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

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

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

for nn being Nat st m <= nn holds

|.(((delta T2) . nn) - 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 nn being Nat st m <= nn holds

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

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

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

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

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

|.(((delta S2) . n) - 0).| < e / 2 by A174, A176;

then ( 0 <= delta (S2 . n) & |.(delta (S2 . n)).| < e / 2 ) by INTEGRA3:9, INTEGRA3:def 2;

then A177: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) < e / 2 by ABSVALUE:def 1;

A178: for y being Real st y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) holds

y < e

proof

max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))
by XXREAL_2:def 8;
reconsider D = T2 . n as Division of ['c,b'] ;

let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) implies y < e )

assume y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) ; :: thesis: y < e

then consider x being object such that

A179: x in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) and

A180: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A179;

A181: x in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) by A179, FINSEQ_1:def 3;

consider E1 being Division of ['c,b'] such that

A182: E1 = S2 . n and

A183: 2 <= len E1 by A30;

set i1 = i + 1;

consider E being Division of ['c,b'] such that

A184: E = S2 . n and

A185: T2 . n = E /^ 1 by A38;

A186: 1 <= len E1 by A183, XXREAL_0:2;

then A187: len D = (len E) - 1 by A184, A185, A182, RFINSEQ:def 1;

A188: len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = len D by INTEGRA1:def 6;

then A189: dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = dom D by FINSEQ_3:29;

end;let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) implies y < e )

assume y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) ; :: thesis: y < e

then consider x being object such that

A179: x in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) and

A180: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A179;

A181: x in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) by A179, FINSEQ_1:def 3;

consider E1 being Division of ['c,b'] such that

A182: E1 = S2 . n and

A183: 2 <= len E1 by A30;

set i1 = i + 1;

consider E being Division of ['c,b'] such that

A184: E = S2 . n and

A185: T2 . n = E /^ 1 by A38;

A186: 1 <= len E1 by A183, XXREAL_0:2;

then A187: len D = (len E) - 1 by A184, A185, A182, RFINSEQ:def 1;

A188: len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = len D by INTEGRA1:def 6;

then A189: dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = dom D by FINSEQ_3:29;

A190: now :: thesis: ( i = 1 implies y < e )

A203:
y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . n),i))))) * (vol (divset ((T2 . n),i)))
by A179, A180, A189, INTEGRA1:def 6;
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E
by A184, INTEGRA1:def 6;

then 2 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A184, A182, A183;

then 2 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def 8;

then A191: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 < e / 2 by A177, XXREAL_0:2;

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

then A193: 1 in dom D by A181, A188, FINSEQ_1:def 3;

len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by A184, A187, INTEGRA1:def 6;

then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def 6;

then 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A181, A192, FINSEQ_2:8;

then 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def 8;

then A194: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 < e / 2 by A177, XXREAL_0:2;

A195: 2 in dom E by A184, A182, A183, FINSEQ_3:25;

1 in Seg (len E) by A184, A182, A186;

then A196: 1 in dom E by FINSEQ_1:def 3;

divset ((S2 . n),1) = [.(lower_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),1))).] by INTEGRA1:4;

then A197: divset ((S2 . n),1) = [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] by A184, A196, INTEGRA1:def 4;

then A198: [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]).] by INTEGRA1:4;

A199: divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),1))),(upper_bound (divset ((T2 . n),1))).] by A192, INTEGRA1:4

.= [.(lower_bound ['c,b']),(upper_bound (divset ((T2 . n),1))).] by A193, INTEGRA1:def 4

.= [.(lower_bound ['c,b']),(D . 1).] by A193, INTEGRA1:def 4

.= [.(lower_bound ['c,b']),(E . (1 + 1)).] by A184, A185, A182, A186, A193, RFINSEQ:def 1

.= [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] by A184, A195, INTEGRA1:def 4 ;

then [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;

then A200: ( lower_bound ['c,b'] = lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] & upper_bound (divset ((S2 . n),2)) = upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] ) by A199, INTEGRA1:5;

y = vol (divset ((T2 . n),1)) by A179, A180, A189, A192, INTEGRA1:20;

then y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + ((upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]) - (lower_bound ['c,b'])) by A192, A199, A200, A197;

then A201: y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + (vol (divset ((S2 . n),1))) by A197, A198, INTEGRA1:5;

divset ((S2 . n),2) = [.(lower_bound (divset ((S2 . n),2))),(upper_bound (divset ((S2 . n),2))).] by INTEGRA1:4;

then divset ((S2 . n),2) = [.(E . (2 - 1)),(upper_bound (divset ((S2 . n),2))).] by A184, A195, INTEGRA1:def 4;

then A202: divset ((S2 . n),2) = [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] by A184, A196, INTEGRA1:def 4;

then [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;

then y = (vol (divset ((S2 . n),2))) + (vol (divset ((S2 . n),1))) by A202, A201, INTEGRA1:5;

then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + (vol (divset ((S2 . n),1))) by A184, A195, INTEGRA1:20;

then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1) by A184, A196, INTEGRA1:20;

then y < (e / 2) + (e / 2) by A191, A194, XREAL_1:8;

hence y < e ; :: thesis: verum

end;then 2 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A184, A182, A183;

then 2 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def 8;

then A191: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 < e / 2 by A177, XXREAL_0:2;

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

then A193: 1 in dom D by A181, A188, FINSEQ_1:def 3;

len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by A184, A187, INTEGRA1:def 6;

then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def 6;

then 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A181, A192, FINSEQ_2:8;

then 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def 3;

then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def 8;

then A194: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 < e / 2 by A177, XXREAL_0:2;

A195: 2 in dom E by A184, A182, A183, FINSEQ_3:25;

1 in Seg (len E) by A184, A182, A186;

then A196: 1 in dom E by FINSEQ_1:def 3;

divset ((S2 . n),1) = [.(lower_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),1))).] by INTEGRA1:4;

then A197: divset ((S2 . n),1) = [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] by A184, A196, INTEGRA1:def 4;

then A198: [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]).] by INTEGRA1:4;

A199: divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),1))),(upper_bound (divset ((T2 . n),1))).] by A192, INTEGRA1:4

.= [.(lower_bound ['c,b']),(upper_bound (divset ((T2 . n),1))).] by A193, INTEGRA1:def 4

.= [.(lower_bound ['c,b']),(D . 1).] by A193, INTEGRA1:def 4

.= [.(lower_bound ['c,b']),(E . (1 + 1)).] by A184, A185, A182, A186, A193, RFINSEQ:def 1

.= [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] by A184, A195, INTEGRA1:def 4 ;

then [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;

then A200: ( lower_bound ['c,b'] = lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] & upper_bound (divset ((S2 . n),2)) = upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] ) by A199, INTEGRA1:5;

y = vol (divset ((T2 . n),1)) by A179, A180, A189, A192, INTEGRA1:20;

then y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + ((upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]) - (lower_bound ['c,b'])) by A192, A199, A200, A197;

then A201: y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + (vol (divset ((S2 . n),1))) by A197, A198, INTEGRA1:5;

divset ((S2 . n),2) = [.(lower_bound (divset ((S2 . n),2))),(upper_bound (divset ((S2 . n),2))).] by INTEGRA1:4;

then divset ((S2 . n),2) = [.(E . (2 - 1)),(upper_bound (divset ((S2 . n),2))).] by A184, A195, INTEGRA1:def 4;

then A202: divset ((S2 . n),2) = [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] by A184, A196, INTEGRA1:def 4;

then [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;

then y = (vol (divset ((S2 . n),2))) + (vol (divset ((S2 . n),1))) by A202, A201, INTEGRA1:5;

then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + (vol (divset ((S2 . n),1))) by A184, A195, INTEGRA1:20;

then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1) by A184, A196, INTEGRA1:20;

then y < (e / 2) + (e / 2) by A191, A194, XREAL_1:8;

hence y < e ; :: thesis: verum

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

hence
y < e
by A190; :: thesis: verum
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1
by A184, A187, INTEGRA1:def 6;

then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def 6;

then A204: i + 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A181, FINSEQ_1:60;

then A205: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;

A206: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A204, FINSEQ_1:def 3;

A207: i in dom D by A181, A188, FINSEQ_1:def 3;

Seg ((len D) + 1) = Seg (len E) by A187;

then i + 1 in Seg (len E) by A181, A188, FINSEQ_1:60;

then A208: i + 1 in dom E by FINSEQ_1:def 3;

len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by A184, INTEGRA1:def 6;

then A209: dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = dom E by FINSEQ_3:29;

assume A210: i <> 1 ; :: thesis: y < e

i in Seg (len D) by A179, A188, FINSEQ_1:def 3;

then 1 <= i by FINSEQ_1:1;

then A211: 1 < i by A210, XXREAL_0:1;

then A212: i - 1 in Seg (len D) by A181, A188, FINSEQ_3:12;

then A213: i - 1 in dom D by FINSEQ_1:def 3;

reconsider i9 = i - 1 as Element of NAT by A212;

1 + 1 < i + 1 by A211, XREAL_1:8;

then A214: i + 1 <> 1 ;

divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),i))),(upper_bound (divset ((T2 . n),i))).] by INTEGRA1:4

.= [.(D . (i - 1)),(upper_bound (divset ((T2 . n),i))).] by A210, A207, INTEGRA1:def 4

.= [.(D . (i - 1)),(D . i).] by A210, A207, INTEGRA1:def 4

.= [.(E . (i9 + 1)),(D . i).] by A184, A185, A182, A186, A213, RFINSEQ:def 1

.= [.(E . ((i - 1) + 1)),(E . (i + 1)).] by A184, A185, A182, A186, A207, RFINSEQ:def 1

.= [.(E . ((i + 1) - 1)),(upper_bound (divset ((S2 . n),(i + 1)))).] by A184, A214, A208, INTEGRA1:def 4

.= [.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).] by A184, A214, A208, INTEGRA1:def 4

.= divset ((S2 . n),(i + 1)) by INTEGRA1:4 ;

then y = (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . (i + 1) by A203, A184, A205, A209, INTEGRA1:def 6;

then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A206, FUNCT_1:def 3;

then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(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 len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def 6;

then A204: i + 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A181, FINSEQ_1:60;

then A205: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;

A206: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A204, FINSEQ_1:def 3;

A207: i in dom D by A181, A188, FINSEQ_1:def 3;

Seg ((len D) + 1) = Seg (len E) by A187;

then i + 1 in Seg (len E) by A181, A188, FINSEQ_1:60;

then A208: i + 1 in dom E by FINSEQ_1:def 3;

len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by A184, INTEGRA1:def 6;

then A209: dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = dom E by FINSEQ_3:29;

assume A210: i <> 1 ; :: thesis: y < e

i in Seg (len D) by A179, A188, FINSEQ_1:def 3;

then 1 <= i by FINSEQ_1:1;

then A211: 1 < i by A210, XXREAL_0:1;

then A212: i - 1 in Seg (len D) by A181, A188, FINSEQ_3:12;

then A213: i - 1 in dom D by FINSEQ_1:def 3;

reconsider i9 = i - 1 as Element of NAT by A212;

1 + 1 < i + 1 by A211, XREAL_1:8;

then A214: i + 1 <> 1 ;

divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),i))),(upper_bound (divset ((T2 . n),i))).] by INTEGRA1:4

.= [.(D . (i - 1)),(upper_bound (divset ((T2 . n),i))).] by A210, A207, INTEGRA1:def 4

.= [.(D . (i - 1)),(D . i).] by A210, A207, INTEGRA1:def 4

.= [.(E . (i9 + 1)),(D . i).] by A184, A185, A182, A186, A213, RFINSEQ:def 1

.= [.(E . ((i - 1) + 1)),(E . (i + 1)).] by A184, A185, A182, A186, A207, RFINSEQ:def 1

.= [.(E . ((i + 1) - 1)),(upper_bound (divset ((S2 . n),(i + 1)))).] by A184, A214, A208, INTEGRA1:def 4

.= [.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).] by A184, A214, A208, INTEGRA1:def 4

.= divset ((S2 . n),(i + 1)) by INTEGRA1:4 ;

then y = (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . (i + 1) by A203, A184, A205, A209, INTEGRA1:def 6;

then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A206, FUNCT_1:def 3;

then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(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

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) . nn) - 0).| < e by INTEGRA3:def 2; :: thesis: verum

then A216: lim (delta T2) = 0 by A172, SEQ_2:def 7;

then A217: ( upper_sum ((f || ['c,b']),T2) is convergent & lim (upper_sum ((f || ['c,b']),T2)) = upper_integral (f || ['c,b']) ) by A166, A18, A215, INTEGRA4:9;

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

ex n being Nat st

for mm being Nat st n <= mm holds

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

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

for mm being Nat st n <= mm holds

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

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

for mm being Nat st n <= mm holds

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

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

for mm being Nat st n <= mm holds

|.(((delta T) . mm) - 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 mm being Nat st n <= mm holds

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

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

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

reconsider m = mm as Element of NAT by ORDINAL1:def 12;

n2 <= n by XXREAL_0:25;

then n2 <= m by A222, XXREAL_0:2;

then |.(((delta T2) . m) - 0).| < e by A221;

then A223: |.(delta (T2 . m)).| < e by INTEGRA3:def 2;

0 <= delta (T2 . m) by INTEGRA3:9;

then A224: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) < e by A223, ABSVALUE:def 1;

n1 <= n by XXREAL_0:25;

then n1 <= m by A222, XXREAL_0:2;

then |.(((delta T1) . m) - 0).| < e by A220;

then A225: |.(delta (T1 . m)).| < e by INTEGRA3:def 2;

0 <= delta (T1 . m) by INTEGRA3:9;

then A226: max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) < e by A225, ABSVALUE:def 1;

A227: for r being Real st r in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) holds

r < e

max (rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) by XXREAL_2:def 8;

then delta (T . m) < e by A227;

then |.(delta (T . m)).| < e by A252, ABSVALUE:def 1;

hence |.(((delta T) . mm) - 0).| < e by INTEGRA3:def 2; :: thesis: verum

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

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

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

for mm being Nat st n <= mm holds

|.(((delta T) . mm) - 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 mm being Nat st n <= mm holds

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

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

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

reconsider m = mm as Element of NAT by ORDINAL1:def 12;

n2 <= n by XXREAL_0:25;

then n2 <= m by A222, XXREAL_0:2;

then |.(((delta T2) . m) - 0).| < e by A221;

then A223: |.(delta (T2 . m)).| < e by INTEGRA3:def 2;

0 <= delta (T2 . m) by INTEGRA3:9;

then A224: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) < e by A223, ABSVALUE:def 1;

n1 <= n by XXREAL_0:25;

then n1 <= m by A222, XXREAL_0:2;

then |.(((delta T1) . m) - 0).| < e by A220;

then A225: |.(delta (T1 . m)).| < e by INTEGRA3:def 2;

0 <= delta (T1 . m) by INTEGRA3:9;

then A226: max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) < e by A225, ABSVALUE:def 1;

A227: for r being Real st r in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) holds

r < e

proof

A252:
0 <= delta (T . m)
by INTEGRA3:9;
reconsider Tm = T . m as Division of ['a,b'] ;

let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) implies y < e )

assume y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) ; :: thesis: y < e

then consider x being object such that

A228: x in dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) and

A229: y = (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A228;

A230: x in Seg (len (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) by A228, FINSEQ_1:def 3;

then A231: 1 <= i by FINSEQ_1:1;

A232: len (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = len Tm by INTEGRA1:def 6;

then A233: i <= len Tm by A230, FINSEQ_1:1;

dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = dom Tm by A232, FINSEQ_3:29;

then A234: y = (upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((T . m),i))))) * (vol (divset ((T . m),i))) by A228, A229, INTEGRA1:def 6;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A235: S1 = T1 . m and

A236: S2 = T2 . m and

A237: T . m = S1 ^ S2 by A93;

A238: len Tm = (len S1) + (len S2) by A237, FINSEQ_1:22;

end;let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) implies y < e )

assume y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) ; :: thesis: y < e

then consider x being object such that

A228: x in dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) and

A229: y = (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A228;

A230: x in Seg (len (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) by A228, FINSEQ_1:def 3;

then A231: 1 <= i by FINSEQ_1:1;

A232: len (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = len Tm by INTEGRA1:def 6;

then A233: i <= len Tm by A230, FINSEQ_1:1;

dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = dom Tm by A232, FINSEQ_3:29;

then A234: y = (upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((T . m),i))))) * (vol (divset ((T . m),i))) by A228, A229, INTEGRA1:def 6;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A235: S1 = T1 . m and

A236: S2 = T2 . m and

A237: T . m = S1 ^ S2 by A93;

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 ((chi (['a,c'],['a,c'])),(T1 . m))) = len S1 by A235, INTEGRA1:def 6;

then A241: i in dom (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A239, FINSEQ_1:def 3;

A242: divset ((T1 . m),i) = divset ((T . m),i) by A95, A235, A239;

A243: divset ((T1 . m),i) c= ['a,c'] by A139, A235, A239;

then divset ((T1 . m),i) c= ['a,b'] by A137;

then (chi (['a,c'],['a,c'])) | (divset ((T1 . m),i)) = (chi (['a,b'],['a,b'])) | (divset ((T . m),i)) by A242, A243, Th4;

then y = (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) . i by A234, A235, A240, A242, INTEGRA1:def 6;

then y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A241, FUNCT_1:def 3;

then y <= max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) by XXREAL_2:def 8;

hence y < e by A226, XXREAL_0:2; :: thesis: verum

end;then A240: i in dom S1 by FINSEQ_1:def 3;

len (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) = len S1 by A235, INTEGRA1:def 6;

then A241: i in dom (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A239, FINSEQ_1:def 3;

A242: divset ((T1 . m),i) = divset ((T . m),i) by A95, A235, A239;

A243: divset ((T1 . m),i) c= ['a,c'] by A139, A235, A239;

then divset ((T1 . m),i) c= ['a,b'] by A137;

then (chi (['a,c'],['a,c'])) | (divset ((T1 . m),i)) = (chi (['a,b'],['a,b'])) | (divset ((T . m),i)) by A242, A243, Th4;

then y = (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) . i by A234, A235, A240, A242, INTEGRA1:def 6;

then y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A241, FUNCT_1:def 3;

then y <= max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) by XXREAL_2:def 8;

hence y < e by A226, 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;

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

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 A112, A235, A236, A247;

A250: divset ((T2 . m),(1 + k)) c= ['c,b'] by A134, A236, A247;

then divset ((T2 . m),(1 + k)) c= ['a,b'] by A17;

then y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k)))) by A234, A245, A249, A250, Th4;

then A251: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) . (1 + k) by A236, A248, INTEGRA1:def 6;

len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) = len S2 by A236, INTEGRA1:def 6;

then 1 + k in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A247, FINSEQ_1:def 3;

then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A251, FUNCT_1:def 3;

then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(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;

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

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 A112, A235, A236, A247;

A250: divset ((T2 . m),(1 + k)) c= ['c,b'] by A134, A236, A247;

then divset ((T2 . m),(1 + k)) c= ['a,b'] by A17;

then y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k)))) by A234, A245, A249, A250, Th4;

then A251: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) . (1 + k) by A236, A248, INTEGRA1:def 6;

len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) = len S2 by A236, INTEGRA1:def 6;

then 1 + k in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A247, FINSEQ_1:def 3;

then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A251, FUNCT_1:def 3;

then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) by XXREAL_2:def 8;

hence y < e by A224, XXREAL_0:2; :: thesis: verum

max (rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) by XXREAL_2:def 8;

then delta (T . m) < e by A227;

then |.(delta (T . m)).| < e by A252, ABSVALUE:def 1;

hence |.(((delta T) . mm) - 0).| < e by INTEGRA3:def 2; :: thesis: verum

then A254: lim (delta T) = 0 by A218, SEQ_2:def 7;

(f || ['a,b']) | ['a,b'] is bounded by A4;

then A255: upper_integral (f || ['a,b']) = lim (upper_sum ((f || ['a,b']),T)) by A12, A253, A254, INTEGRA4:9;

A256: for i being Element of NAT holds lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i)))

proof

A278:
for i being Element of NAT holds Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i))))
let i be Element of NAT ; :: thesis: lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i)))

reconsider F = lower_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;

reconsider F1 = lower_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;

reconsider F2 = lower_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;

reconsider S = T . i as Division of ['a,b'] ;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A257: S1 = T1 . i and

A258: S2 = T2 . i and

A259: T . i = S1 ^ S2 by A93;

A260: len F = len S by INTEGRA1:def 7

.= (len S1) + (len S2) by A259, FINSEQ_1:22

.= (len F1) + (len S2) by A257, INTEGRA1:def 7 ;

then A261: len F = (len F1) + (len F2) by A258, INTEGRA1:def 7;

hence lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A271, A262, FINSEQ_1:def 7; :: thesis: verum

end;reconsider F = lower_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;

reconsider F1 = lower_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;

reconsider F2 = lower_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;

reconsider S = T . i as Division of ['a,b'] ;

consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that

A257: S1 = T1 . i and

A258: S2 = T2 . i and

A259: T . i = S1 ^ S2 by A93;

A260: len F = len S by INTEGRA1:def 7

.= (len S1) + (len S2) by A259, FINSEQ_1:22

.= (len F1) + (len S2) by A257, INTEGRA1:def 7 ;

then A261: len F = (len F1) + (len F2) by A258, INTEGRA1:def 7;

A262: now :: thesis: for k being Nat st k in dom F2 holds

F . ((len F1) + k) = F2 . k

F . ((len F1) + k) = F2 . k

let k be Nat; :: thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )

assume k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k

then A263: k in Seg (len F2) by FINSEQ_1:def 3;

then 1 <= k by FINSEQ_1:1;

then A264: 1 + (len F1) <= k + (len F1) by XREAL_1:6;

k <= len F2 by A263, FINSEQ_1:1;

then A265: (len F1) + k <= len F by A261, XREAL_1:6;

1 <= 1 + (len F1) by NAT_1:11;

then 1 <= k + (len F1) by A264, XXREAL_0:2;

then k + (len F1) in Seg (len F) by A265;

then (len F1) + k in Seg (len S) by INTEGRA1:def 7;

then (len F1) + k in dom S by FINSEQ_1:def 3;

then A266: F . ((len F1) + k) = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 7;

A267: k in Seg (len S2) by A258, A263, INTEGRA1:def 7;

then A268: k in dom S2 by FINSEQ_1:def 3;

len F1 = len S1 by A257, INTEGRA1:def 7;

then A269: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A257, A258, A267;

A270: divset ((T2 . i),k) c= ['c,b'] by A134, A258, A267;

then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17, A269;

then F . ((len F1) + k) = (lower_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A266, A269, A270, Th3;

hence F . ((len F1) + k) = F2 . k by A258, A268, INTEGRA1:def 7; :: thesis: verum

end;assume k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k

then A263: k in Seg (len F2) by FINSEQ_1:def 3;

then 1 <= k by FINSEQ_1:1;

then A264: 1 + (len F1) <= k + (len F1) by XREAL_1:6;

k <= len F2 by A263, FINSEQ_1:1;

then A265: (len F1) + k <= len F by A261, XREAL_1:6;

1 <= 1 + (len F1) by NAT_1:11;

then 1 <= k + (len F1) by A264, XXREAL_0:2;

then k + (len F1) in Seg (len F) by A265;

then (len F1) + k in Seg (len S) by INTEGRA1:def 7;

then (len F1) + k in dom S by FINSEQ_1:def 3;

then A266: F . ((len F1) + k) = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 7;

A267: k in Seg (len S2) by A258, A263, INTEGRA1:def 7;

then A268: k in dom S2 by FINSEQ_1:def 3;

len F1 = len S1 by A257, INTEGRA1:def 7;

then A269: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A257, A258, A267;

A270: divset ((T2 . i),k) c= ['c,b'] by A134, A258, A267;

then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17, A269;

then F . ((len F1) + k) = (lower_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A266, A269, A270, Th3;

hence F . ((len F1) + k) = F2 . k by A258, A268, INTEGRA1:def 7; :: thesis: verum

A271: now :: thesis: for k being Nat st k in dom F1 holds

F . k = F1 . k

dom F = Seg ((len F1) + (len F2))
by A261, FINSEQ_1:def 3;F . k = F1 . k

let k be Nat; :: thesis: ( k in dom F1 implies F . k = F1 . k )

len (lower_volume ((f || ['a,b']),(T . i))) = len S by INTEGRA1:def 7;

then A272: dom (lower_volume ((f || ['a,b']),(T . i))) = dom S by FINSEQ_3:29;

assume A273: k in dom F1 ; :: thesis: F . k = F1 . k

then k in Seg (len F1) by FINSEQ_1:def 3;

then A274: k in Seg (len S1) by A257, INTEGRA1:def 7;

then A275: k in dom S1 by FINSEQ_1:def 3;

len F1 <= len F by A260, NAT_1:11;

then dom F1 c= dom F by FINSEQ_3:30;

then A276: F . k = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by A273, A272, INTEGRA1:def 7;

A277: ( divset ((T . i),k) = divset ((T1 . i),k) & divset ((T1 . i),k) c= ['a,c'] ) by A139, A95, A257, A274;

then divset ((T . i),k) c= ['a,b'] by A137;

then F . k = (lower_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A276, A277, Th3;

hence F . k = F1 . k by A257, A275, INTEGRA1:def 7; :: thesis: verum

end;len (lower_volume ((f || ['a,b']),(T . i))) = len S by INTEGRA1:def 7;

then A272: dom (lower_volume ((f || ['a,b']),(T . i))) = dom S by FINSEQ_3:29;

assume A273: k in dom F1 ; :: thesis: F . k = F1 . k

then k in Seg (len F1) by FINSEQ_1:def 3;

then A274: k in Seg (len S1) by A257, INTEGRA1:def 7;

then A275: k in dom S1 by FINSEQ_1:def 3;

len F1 <= len F by A260, NAT_1:11;

then dom F1 c= dom F by FINSEQ_3:30;

then A276: F . k = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by A273, A272, INTEGRA1:def 7;

A277: ( divset ((T . i),k) = divset ((T1 . i),k) & divset ((T1 . i),k) c= ['a,c'] ) by A139, A95, A257, A274;

then divset ((T . i),k) c= ['a,b'] by A137;

then F . k = (lower_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A276, A277, Th3;

hence F . k = F1 . k by A257, A275, INTEGRA1:def 7; :: thesis: verum

hence lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A271, A262, FINSEQ_1:def 7; :: thesis: verum

proof

let i be Element of NAT ; :: thesis: Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i))))

lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A256;

hence Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum

end;lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A256;

hence Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum

now :: thesis: for i being Nat holds (lower_sum ((f || ['a,b']),T)) . i = ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i)

then A279:
lower_sum ((f || ['a,b']),T) = (lower_sum ((f || ['a,c']),T1)) + (lower_sum ((f || ['c,b']),T2))
by SEQ_1:7;let i be Nat; :: thesis: (lower_sum ((f || ['a,b']),T)) . i = ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i)

reconsider ii = i as Element of NAT by ORDINAL1:def 12;

thus (lower_sum ((f || ['a,b']),T)) . i = lower_sum ((f || ['a,b']),(T . ii)) by INTEGRA2:def 3

.= (lower_sum ((f || ['a,c']),(T1 . ii))) + (Sum (lower_volume ((f || ['c,b']),(T2 . ii)))) by A278

.= ((lower_sum ((f || ['a,c']),T1)) . i) + (lower_sum ((f || ['c,b']),(T2 . ii))) by INTEGRA2:def 3

.= ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def 3 ; :: thesis: verum

end;reconsider ii = i as Element of NAT by ORDINAL1:def 12;

thus (lower_sum ((f || ['a,b']),T)) . i = lower_sum ((f || ['a,b']),(T . ii)) by INTEGRA2:def 3

.= (lower_sum ((f || ['a,c']),(T1 . ii))) + (Sum (lower_volume ((f || ['c,b']),(T2 . ii)))) by A278

.= ((lower_sum ((f || ['a,c']),T1)) . i) + (lower_sum ((f || ['c,b']),(T2 . ii))) by INTEGRA2:def 3

.= ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def 3 ; :: thesis: verum

A280: f || ['a,c'] is Function of ['a,c'],REAL by A2, A137, Lm1, XBOOLE_1:1;

then A281: ( f || ['a,c'] is upper_integrable & f || ['a,c'] is lower_integrable ) by A138, INTEGRA4:10;

A282: ( upper_sum ((f || ['a,c']),T1) is convergent & lim (upper_sum ((f || ['a,c']),T1)) = upper_integral (f || ['a,c']) ) by A280, A138, A53, INTEGRA4:9;

then A283: (upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b']) by A165, A217, A255, SEQ_2:6;

A284: ( lower_sum ((f || ['a,c']),T1) is convergent & lim (lower_sum ((f || ['a,c']),T1)) = lower_integral (f || ['a,c']) ) by A280, A138, A53, INTEGRA4:8;

(f || ['a,b']) | ['a,b'] is bounded by A4;

then A285: lower_integral (f || ['a,b']) = lim (lower_sum ((f || ['a,b']),T)) by A12, A253, A254, INTEGRA4:8;

( lower_sum ((f || ['c,b']),T2) is convergent & lim (lower_sum ((f || ['c,b']),T2)) = lower_integral (f || ['c,b']) ) by A166, A18, A215, A216, INTEGRA4:8;

then A286: (lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b']) by A279, A284, A285, SEQ_2:6;

integral (f,a,b) = integral (f,['a,b']) by A1, INTEGRA5:def 4

.= (integral (f || ['a,c'])) + (integral (f || ['c,b'])) by A165, A282, A217, A255, SEQ_2:6 ;

hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A58, A57; :: thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )

f || ['a,b'] is integrable by A3;

then A287: upper_integral (f || ['a,b']) = lower_integral (f || ['a,b']) ;

A288: ( f || ['c,b'] is upper_integrable & f || ['c,b'] is lower_integrable ) by A166, A18, INTEGRA4:10;

A289: lower_integral (f || ['a,c']) <= upper_integral (f || ['a,c']) by A280, A138, INTEGRA1:49;

then lower_integral (f || ['c,b']) = upper_integral (f || ['c,b']) by A287, A283, A286, A167, Th1;

then A290: f || ['c,b'] is integrable by A288;

lower_integral (f || ['a,c']) = upper_integral (f || ['a,c']) by A287, A283, A286, A289, A167, Th1;

then f || ['a,c'] is integrable by A281;

hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) by A290; :: thesis: verum