let a, b, c be real number ; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
assume A1: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c ) ; :: thesis:
A2: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
then A3: ( a <= c & c <= b ) by A1, XXREAL_1:1;
then A4: ( ['a,c'] = [.a,c.] & ['c,b'] = [.c,b.] ) by INTEGRA5:def 4;
then A5: ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) by A2, A3, XXREAL_1:34;
( [.a,b.] = [.(inf [.a,b.]),(sup [.a,b.]).] & [.c,b.] = [.(inf [.c,b.]),(sup [.c,b.]).] & [.a,c.] = [.(inf [.a,c.]),(sup [.a,c.]).] ) by A2, A4, INTEGRA1:5;
then A6: ( inf ['a,b'] = a & sup ['a,b'] = b & inf ['c,b'] = c & sup ['c,b'] = b & inf ['a,c'] = a & sup ['a,c'] = c ) by A2, A4, INTEGRA1:6;
set FAB = f || ['a,b'];
set FAC = f || ['a,c'];
set FCB = f || ['c,b'];
A7: ( f || ['a,b'] is Function of ['a,b'],REAL & f || ['a,c'] is Function of ['a,c'],REAL & f || ['c,b'] is Function of ['c,b'],REAL ) by A1, A5, Lm1, XBOOLE_1:1;
f || ['a,b'] is integrable by A1, INTEGRA5:def 2;
then A8: ( f || ['a,b'] is upper_integrable & f || ['a,b'] is lower_integrable & upper_integral (f || ['a,b']) = lower_integral (f || ['a,b']) ) by INTEGRA1:def 17;
( f | ['a,c'] is bounded & f | ['c,b'] is bounded ) by A1, A5, RFUNCT_1:91;
then A10: ( (f || ['a,c']) | ['a,c'] is bounded & (f || ['c,b']) | ['c,b'] is bounded ) by INTEGRA5:9;
consider T1 being DivSequence of ['a,c'] such that
A11: ( delta T1 is convergent & lim (delta T1) = 0 ) by INTEGRA4:11;
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

c < b by A1, A3, XXREAL_0:1;
then vol ['c,b'] > 0 by A6, XREAL_1:52;
then consider T being DivSequence of ['c,b'] such that
A12: ( delta T is convergent & lim (delta T) = 0 & ( 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:

now

let i be Element of NAT ; :: thesis:
assume A13: 2 <= i ; :: thesis:
consider Tn being Division of ['c,b'] such that
A14: ( Tn divide_into_equal i + 1 & T . i = Tn ) by A12;
reconsider Tn = Tn as Division of ['c,b'] ;
take Tn = Tn; :: thesis:
thus Tn = T . i by A14; :: thesis:
len Tn = i + 1 by A14, INTEGRA4:def 1;
then i <= len Tn by NAT_1:11;
hence 2 <= len Tn by A13, XXREAL_0:2; :: thesis:

end;

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

end;

then consider PS2 being DivSequence of ['c,b'] such that
A15: ( 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 ) ) ;
consider K being Element of NAT such that
A16: 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 A15;
defpred S₁[ 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) );
A17: for n being Element of NAT ex D being Element of divs ['c,b'] st S₁[n,D]

proof

let n be Element of NAT ; :: thesis:
reconsider D = PS2 . (n + K) as Element of divs ['c,b'] by INTEGRA1:def 3;
take D ; :: thesis:
thus S₁[n,D] ; :: thesis:

end;

consider S2 being Function of NAT ,(divs ['c,b']) such that
A18: for n being Element of NAT holds S₁[n,S2 . n] from FUNCT_2:sch 3(A17);
reconsider S2 = S2 as DivSequence of ['c,b'] ;
A19: ( ( for i being Element of NAT ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i ) ) & delta S2 is convergent & lim (delta S2) = 0 )

proof

A20: now

let i be Element of NAT ; :: thesis:
A21: K <= i + K by NAT_1:11;
ex n being Element of NAT ex e being Division of ['c,b'] st
( n = i & e = S2 . i & e = PS2 . (n + K) ) by A18;
hence ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i ) by A16, A21; :: thesis:

end;

( delta S2 is convergent & lim (delta S2) = 0 )

proof

A22: now

let e be real number ; :: thesis:
assume 0 < e ; :: thesis:
then consider m being Element of NAT such that
A23: for n being Element of NAT st m <= n holds
abs (((delta PS2) . n) - 0 ) < e by A15, SEQ_2:def 7;
take m = m; :: thesis:

hereby :: thesis:

let n be Element of NAT ; :: thesis:
assume A24: m <= n ; :: thesis:
n <= n + K by NAT_1:11;
then m <= n + K by A24, XXREAL_0:2;
then abs (((delta PS2) . (n + K)) - 0 ) < e by A23;
then A25: abs ((delta (PS2 . (n + K))) - 0 ) < e by INTEGRA2:def 3;
ex k being Element of NAT ex e1 being Division of ['c,b'] st
( k = n & e1 = S2 . n & e1 = PS2 . (k + K) ) by A18;
hence abs (((delta S2) . n) - 0 ) < e by A25, INTEGRA2:def 3; :: thesis:

end;

hence delta S2 is convergent by SEQ_2:def 6; :: thesis:
hence lim (delta S2) = 0 by A22, SEQ_2:def 7; :: thesis:

end;

hence ( ( for i being Element of NAT ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i ) ) & delta S2 is convergent & lim (delta S2) = 0 ) by A20; :: thesis:

end;

defpred S₂[ Element of NAT , set ] means ex S being Division of ['c,b'] st
( S = S2 . $1 & $2 = S /^ 1 );
A26: for i being Element of NAT ex T being Element of divs ['c,b'] st S₂[i,T]

proof

let i be Element of NAT ; :: thesis:
consider S being Division of ['c,b'] such that
A27: ( S = S2 . i & 2 <= len S ) by A19;
set T = S /^ 1;
A28: ( rng S c= ['c,b'] & S . (len S) = sup ['c,b'] ) by INTEGRA1:def 2;
A29: 1 <= len S by A27, XXREAL_0:2;
2 - 1 <= (len S) - 1 by A27, XREAL_1:15;
then A30: 1 <= len (S /^ 1) by A29, RFINSEQ:def 2;
then A31: ( not S /^ 1 is empty & S /^ 1 is increasing ) by A29, INTEGRA1:36;
rng (S /^ 1) c= rng S by FINSEQ_5:36;
then A32: rng (S /^ 1) c= ['c,b'] by A28, XBOOLE_1:1;
len (S /^ 1) in Seg (len (S /^ 1)) by A30;
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 A29, RFINSEQ:def 2;
then (S /^ 1) . (len (S /^ 1)) = S . (((len S) - 1) + 1) by A29, RFINSEQ:def 2;
then (S /^ 1) . (len (S /^ 1)) = sup ['c,b'] by INTEGRA1:def 2;
then S /^ 1 is Division of ['c,b'] by A31, A32, 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₂[i,T] by A27, A31, A32, INTEGRA1:def 2; :: thesis:

end;

consider T2 being DivSequence of ['c,b'] such that
A33: for i being Element of NAT holds S₂[i,T2 . i] from FUNCT_2:sch 3(A26);
A34: for n being Element of NAT ex D being Division of ['c,b'] st
( D = T2 . n & 1 <= len D )

proof

let n be Element of NAT ; :: thesis:
consider E being Division of ['c,b'] such that
A35: ( E = S2 . n & T2 . n = E /^ 1 ) by A33;
reconsider D = T2 . n as Division of ['c,b'] by INTEGRA1:def 3;
take D ; :: thesis:
ex E1 being Division of ['c,b'] st
( E1 = S2 . n & 2 <= len E1 ) by A19;
then ( 1 <= len E & 2 - 1 <= (len E) - 1 ) by A35, XREAL_1:15, XXREAL_0:2;
hence ( D = T2 . n & 1 <= len D ) by A35, RFINSEQ:def 2; :: thesis:

end;

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

let n be Element of NAT ; :: thesis:
consider E being Division of ['c,b'] such that
A37: ( E = S2 . n & T2 . n = E /^ 1 ) by A33;
consider E1 being Division of ['c,b'] such that
A38: ( E1 = S2 . n & 2 <= len E1 ) by A19;
reconsider D = T2 . n as Division of ['c,b'] by INTEGRA1:def 3;
take D ; :: thesis:
A39: 1 <= len E by A37, A38, XXREAL_0:2;
then A40: len D = (len E) - 1 by A37, RFINSEQ:def 2;
2 - 1 <= (len E) - 1 by A37, A38, XREAL_1:15;
then 1 in Seg (len D) by A40;
then A41: 1 in dom D by FINSEQ_1:def 3;
then A42: D . 1 = E . (1 + 1) by A37, A39, RFINSEQ:def 2;
A43: rng E c= ['c,b'] by INTEGRA1:def 2;
( 1 in Seg (len E) & 2 in Seg (len E) ) by A37, A38, A39;
then A44: ( 1 in dom E & 2 in dom E ) by FINSEQ_1:def 3;
then E . 1 in rng E by FUNCT_1:def 5;
then A45: ( c <= E . 1 & E . 1 <= b ) by A4, A43, XXREAL_1:1;
A46: E . 1 < E . 2 by A44, SEQM_3:def 1;
then A47: c < D . 1 by A42, A45, XXREAL_0:2;

now

let i be Element of NAT ; :: thesis:
assume A48: i in dom D ; :: thesis:
then A49: 1 <= i by FINSEQ_3:27;

hereby :: thesis:

assume i <> 1 ; :: thesis:
then 1 < i by A49, XXREAL_0:1;
then D . 1 < D . i by A41, A48, SEQM_3:def 1;
hence c < D . i by A47, XXREAL_0:2; :: thesis:

end;

hence c < D . i by A42, A45, A46, XXREAL_0:2; :: thesis:

end;

hence ( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) ) ; :: thesis:

end;

set XCB = chi ['c,b'],['c,b'];
A50: ( delta T2 is convergent & lim (delta T2) = 0 )

proof

A51: now

let e be real number ; :: thesis:
assume e > 0 ; :: thesis:
then A52: ( 0 < e / 2 & e / 2 < e ) by XREAL_1:217, XREAL_1:218;
then consider m being Element of NAT such that
A53: for n being Element of NAT st m <= n holds
abs (((delta S2) . n) - 0 ) < e / 2 by A19, SEQ_2:def 7;
take m = m; :: thesis:

now

let n be Element of NAT ; :: thesis:
A54: ( 0 <= delta (S2 . n) & 0 <= delta (T2 . n) ) by INTEGRA3:8;
assume m <= n ; :: thesis:
then abs (((delta S2) . n) - 0 ) < e / 2 by A53;
then abs (delta (S2 . n)) < e / 2 by INTEGRA2:def 3;
then A55: max (rng (upper_volume (chi ['c,b'],['c,b']),(S2 . n))) < e / 2 by A54, ABSVALUE:def 1;
A56: for y being real number st y in rng (upper_volume (chi ['c,b'],['c,b']),(T2 . n)) holds
y < e

proof

let y be real number ; :: thesis:
assume y in rng (upper_volume (chi ['c,b'],['c,b']),(T2 . n)) ; :: thesis:
then consider x being set such that
A57: ( x in dom (upper_volume (chi ['c,b'],['c,b']),(T2 . n)) & y = (upper_volume (chi ['c,b'],['c,b']),(T2 . n)) . x ) by FUNCT_1:def 5;
A58: x in Seg (len (upper_volume (chi ['c,b'],['c,b']),(T2 . n))) by A57, FINSEQ_1:def 3;
reconsider i = x as Element of NAT by A57;
reconsider D = T2 . n as Division of ['c,b'] by INTEGRA1:def 3;
A59: len (upper_volume (chi ['c,b'],['c,b']),(T2 . n)) = len D by INTEGRA1:def 7;
then U: dom (upper_volume (chi ['c,b'],['c,b']),(T2 . n)) = dom D by FINSEQ_3:31;
then A60: y = (sup (rng ((chi ['c,b'],['c,b']) | (divset (T2 . n),i)))) * (vol (divset (T2 . n),i)) by A57, INTEGRA1:def 7;
consider E being Division of ['c,b'] such that
A61: ( E = S2 . n & T2 . n = E /^ 1 ) by A33;
consider E1 being Division of ['c,b'] such that
A62: ( E1 = S2 . n & 2 <= len E1 ) by A19;
A63: 1 <= len E1 by A62, XXREAL_0:2;
then A64: len D = (len E) - 1 by A61, A62, RFINSEQ:def 2;
set i1 = i + 1;

A65: now

assume A66: i = 1 ; :: thesis:
then A67: 1 in dom D by A58, A59, FINSEQ_1:def 3;
A69: 2 in dom E by A61, A62, FINSEQ_3:27;
A70: divset (T2 . n),i = [.(inf (divset (T2 . n),1)),(sup (divset (T2 . n),1)).] by A66, INTEGRA1:5
.= [.(inf ['c,b']),(sup (divset (T2 . n),1)).] by A67, INTEGRA1:def 5
.= [.(inf ['c,b']),(D . 1).] by A67, INTEGRA1:def 5
.= [.(inf ['c,b']),(E . (1 + 1)).] by A61, A62, A63, A67, RFINSEQ:def 2
.= [.(inf ['c,b']),(sup (divset (S2 . n),2)).] by A61, A69, INTEGRA1:def 5 ;
then [.(inf ['c,b']),(sup (divset (S2 . n),2)).] = [.(inf [.(inf ['c,b']),(sup (divset (S2 . n),2)).]),(sup [.(inf ['c,b']),(sup (divset (S2 . n),2)).]).] by INTEGRA1:5;
then A71: ( inf ['c,b'] = inf [.(inf ['c,b']),(sup (divset (S2 . n),2)).] & sup (divset (S2 . n),2) = sup [.(inf ['c,b']),(sup (divset (S2 . n),2)).] ) by A70, INTEGRA1:6;
len (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) = len E by A61, INTEGRA1:def 7;
then 2 in Seg (len (upper_volume (chi ['c,b'],['c,b']),(S2 . n))) by A61, A62;
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 5;
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 A72: (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) . 2 < e / 2 by A55, XXREAL_0:2;
len (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) = (len D) + 1 by A61, A64, INTEGRA1:def 7;
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 7;
then 1 in Seg (len (upper_volume (chi ['c,b'],['c,b']),(S2 . n))) by A58, A66, FINSEQ_2:9;
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 5;
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 A73: (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) . 1 < e / 2 by A55, XXREAL_0:2;
1 in Seg (len E) by A61, A62, A63;
then A75: 1 in dom E by FINSEQ_1:def 3;
divset (S2 . n),1 = [.(inf (divset (S2 . n),1)),(sup (divset (S2 . n),1)).] by INTEGRA1:5;
then A76: divset (S2 . n),1 = [.(inf ['c,b']),(sup (divset (S2 . n),1)).] by A61, A75, INTEGRA1:def 5;
then A77: [.(inf ['c,b']),(sup (divset (S2 . n),1)).] = [.(inf [.(inf ['c,b']),(sup (divset (S2 . n),1)).]),(sup [.(inf ['c,b']),(sup (divset (S2 . n),1)).]).] by INTEGRA1:5;
divset (S2 . n),2 = [.(inf (divset (S2 . n),2)),(sup (divset (S2 . n),2)).] by INTEGRA1:5;
then divset (S2 . n),2 = [.(E . (2 - 1)),(sup (divset (S2 . n),2)).] by A61, A69, INTEGRA1:def 5;
then A78: divset (S2 . n),2 = [.(sup (divset (S2 . n),1)),(sup (divset (S2 . n),2)).] by A61, A75, INTEGRA1:def 5;
then A79: [.(sup (divset (S2 . n),1)),(sup (divset (S2 . n),2)).] = [.(inf [.(sup (divset (S2 . n),1)),(sup (divset (S2 . n),2)).]),(sup [.(sup (divset (S2 . n),1)),(sup (divset (S2 . n),2)).]).] by INTEGRA1:5;
y = vol (divset (T2 . n),1) by A57, A66, U, INTEGRA1:22;
then y = ((sup (divset (S2 . n),2)) - (sup (divset (S2 . n),1))) + ((sup [.(inf ['c,b']),(sup (divset (S2 . n),1)).]) - (inf ['c,b'])) by A66, A70, A71, A76;
then y = ((sup (divset (S2 . n),2)) - (sup (divset (S2 . n),1))) + (vol (divset (S2 . n),1)) by A76, A77, INTEGRA1:6;
then y = (vol (divset (S2 . n),2)) + (vol (divset (S2 . n),1)) by A78, A79, INTEGRA1:6;
then y = ((upper_volume (chi ['c,b'],['c,b']),(S2 . n)) . 2) + (vol (divset (S2 . n),1)) by A61, A69, INTEGRA1:22;
then y = ((upper_volume (chi ['c,b'],['c,b']),(S2 . n)) . 2) + ((upper_volume (chi ['c,b'],['c,b']),(S2 . n)) . 1) by A61, A75, INTEGRA1:22;
then y < (e / 2) + (e / 2) by A72, A73, XREAL_1:10;
hence y < e ; :: thesis:

end;

now

assume A80: i <> 1 ; :: thesis:
i in Seg (len D) by A57, A59, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:3;
then A81: 1 < i by A80, XXREAL_0:1;
then A82: i - 1 in Seg (len D) by A58, A59, FINSEQ_3:13;
then A83: i - 1 in dom D by FINSEQ_1:def 3;
reconsider i' = i - 1 as Element of NAT by A82;
1 + 1 < i + 1 by A81, XREAL_1:10;
then A84: i + 1 <> 1 ;
Seg ((len D) + 1) = Seg (len E) by A64;
then i + 1 in Seg (len E) by A58, A59, FINSEQ_1:81;
then A85: i + 1 in dom E by FINSEQ_1:def 3;
A86: i in dom D by A58, A59, FINSEQ_1:def 3;
A87: divset (T2 . n),i = [.(inf (divset (T2 . n),i)),(sup (divset (T2 . n),i)).] by INTEGRA1:5
.= [.(D . (i - 1)),(sup (divset (T2 . n),i)).] by A80, A86, INTEGRA1:def 5
.= [.(D . (i - 1)),(D . i).] by A80, A86, INTEGRA1:def 5
.= [.(E . (i' + 1)),(D . i).] by A61, A62, A63, A83, RFINSEQ:def 2
.= [.(E . ((i - 1) + 1)),(E . (i + 1)).] by A61, A62, A63, A86, RFINSEQ:def 2
.= [.(E . ((i + 1) - 1)),(sup (divset (S2 . n),(i + 1))).] by A61, A84, A85, INTEGRA1:def 5
.= [.(inf (divset (S2 . n),(i + 1))),(sup (divset (S2 . n),(i + 1))).] by A61, A84, A85, INTEGRA1:def 5
.= divset (S2 . n),(i + 1) by INTEGRA1:5 ;
len (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) = (len D) + 1 by A61, A64, INTEGRA1:def 7;
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 7;
then A88: i + 1 in Seg (len (upper_volume (chi ['c,b'],['c,b']),(S2 . n))) by A58, FINSEQ_1:81;
then B88: i + 1 in dom (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) by FINSEQ_1:def 3;
len (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) = len E by A61, INTEGRA1:def 7;
then dom (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) = dom E by FINSEQ_3:31;
then A89: y = (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) . (i + 1) by A60, A61, A87, B88, INTEGRA1:def 7;
i + 1 in dom (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) by A88, FINSEQ_1:def 3;
then y in rng (upper_volume (chi ['c,b'],['c,b']),(S2 . n)) by A89, FUNCT_1:def 5;
then y <= max (rng (upper_volume (chi ['c,b'],['c,b']),(S2 . n))) by XXREAL_2:def 8;
then y < e / 2 by A55, XXREAL_0:2;
hence y < e by A52, XXREAL_0:2; :: thesis:

end;

hence y < e by A65; :: thesis:

end;

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;
then delta (T2 . n) < e by A56;
then abs (delta (T2 . n)) < e by A54, ABSVALUE:def 1;
hence abs (((delta T2) . n) - 0 ) < e by INTEGRA2:def 3; :: thesis:

end;

hence for n being Element of NAT st m <= n holds
abs (((delta T2) . n) - 0 ) < e ; :: thesis:

end;

hence delta T2 is convergent by SEQ_2:def 6; :: thesis:
hence lim (delta T2) = 0 by A51, SEQ_2:def 7; :: thesis:

end;

defpred S₃[ 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 );
A90: for i being Element of NAT ex T being Element of divs ['a,b'] st S₃[i,T]

proof

let i0 be Element of NAT ; :: thesis:
reconsider S1 = T1 . i0 as Division of ['a,c'] by INTEGRA1:def 3;
reconsider S2 = T2 . i0 as Division of ['c,b'] by INTEGRA1:def 3;
set T = S1 ^ S2;
A91: ( rng S1 c= ['a,c'] & S1 . (len S1) = sup ['a,c'] & rng S2 c= ['c,b'] & S2 . (len S2) = sup ['c,b'] ) by INTEGRA1:def 2;
then (rng S1) \/ (rng S2) c= ['a,c'] \/ ['c,b'] by XBOOLE_1:13;
then (rng S1) \/ (rng S2) c= [.a,b.] by A3, A4, XXREAL_1:174;
then A92: rng (S1 ^ S2) c= ['a,b'] by A2, FINSEQ_1:44;
ex D being Division of ['c,b'] st
( D = T2 . i0 & 1 <= len D ) by A34;
then len S2 in Seg (len S2) ;
then A93: len S2 in dom S2 by FINSEQ_1:def 3;
A94: (S1 ^ S2) . (len (S1 ^ S2)) = (S1 ^ S2) . ((len S1) + (len S2)) by FINSEQ_1:35
.= S2 . (len S2) by A93, FINSEQ_1:def 7
.= sup ['a,b'] by A6, INTEGRA1:def 2 ;

now

let i, j be Element of NAT ; :: thesis:
assume A95: ( i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j ) ; :: thesis:
then A96: ( 1 <= i & i <= len (S1 ^ S2) & 1 <= j & j <= len (S1 ^ S2) ) by FINSEQ_3:27;

A97: now

assume A98: j <= len S1 ; :: thesis:
then i <= len S1 by A95, XXREAL_0:2;
then A99: ( i in dom S1 & j in dom S1 ) by A96, A98, FINSEQ_3:27;
then ( (S1 ^ S2) . i = S1 . i & (S1 ^ S2) . j = S1 . j ) by FINSEQ_1:def 7;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A95, A99, SEQM_3:def 1; :: thesis:

end;

now

assume A100: j > len S1 ; :: thesis:
then A101: (S1 ^ S2) . j = S2 . (j - (len S1)) by A96, FINSEQ_1:37;
A102: (len S1) + 1 <= j by A100, NAT_1:13;
then consider m being Nat such that
A103: ((len S1) + 1) + m = j by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
1 + m = j - (len S1) by A103;
then A104: 1 <= 1 + m by A102, XREAL_1:21;
j <= (len S1) + (len S2) by A96, FINSEQ_1:35;
then j - (len S1) <= len S2 by XREAL_1:22;
then 1 + m in Seg (len S2) by A103, A104;
then A105: j - (len S1) in dom S2 by A103, FINSEQ_1:def 3;

A106: now

assume i <= len S1 ; :: thesis:
then A107: i in dom S1 by A96, FINSEQ_3:27;
then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def 7;
then (S1 ^ S2) . i in rng S1 by A107, FUNCT_1:def 5;
then A108: ( a <= (S1 ^ S2) . i & (S1 ^ S2) . i <= c ) by A4, A91, 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 A36;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A101, A105, A108, XXREAL_0:2; :: thesis:

end;

now

assume A109: i > len S1 ; :: thesis:
then A110: (S1 ^ S2) . i = S2 . (i - (len S1)) by A96, FINSEQ_1:37;
A111: i - (len S1) < j - (len S1) by A95, XREAL_1:16;
A112: (len S1) + 1 <= i by A109, NAT_1:13;
then consider m being Nat such that
A113: ((len S1) + 1) + m = i by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
1 + m = i - (len S1) by A113;
then A114: 1 <= 1 + m by A112, XREAL_1:21;
i <= (len S1) + (len S2) by A96, FINSEQ_1:35;
then i - (len S1) <= len S2 by XREAL_1:22;
then 1 + m in Seg (len S2) by A113, A114;
then i - (len S1) in dom S2 by A113, FINSEQ_1:def 3;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A101, A105, A110, A111, SEQM_3:def 1; :: thesis:

end;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A106; :: thesis:

end;

hence (S1 ^ S2) . i < (S1 ^ S2) . j by A97; :: thesis:

end;

then S1 ^ S2 is non empty increasing FinSequence of REAL by SEQM_3:def 1;
then S1 ^ S2 is Division of ['a,b'] by A92, A94, 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₃[i0,T] by INTEGRA1:def 2; :: thesis:

end;

consider T being DivSequence of ['a,b'] such that
A115: for i being Element of NAT holds S₃[i,T . i] from FUNCT_2:sch 3(A90);
A116: 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

let i, k be Element of NAT ; :: thesis:
let S0 be Division of ['a,c']; :: thesis:
assume A117: ( S0 = T1 . i & k in Seg (len S0) ) ; :: thesis:
then k in dom S0 by FINSEQ_1:def 3;
hence divset (T1 . i),k c= ['a,c'] by A117, INTEGRA1:10; :: thesis:

end;

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

let i, k be Element of NAT ; :: thesis:
let S0 be Division of ['c,b']; :: thesis:
assume A119: ( S0 = T2 . i & k in Seg (len S0) ) ; :: thesis:
then k in dom S0 by FINSEQ_1:def 3;
hence divset (T2 . i),k c= ['c,b'] by A119, INTEGRA1:10; :: thesis:

end;

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

let i, k be Element of NAT ; :: thesis:
let S0 be Division of ['a,c']; :: thesis:
assume A121: S0 = T1 . i ; :: thesis:
assume A122: k in Seg (len S0) ; :: thesis:
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A123: ( S1 = T1 . i & S2 = T2 . i & T . i = S1 ^ S2 ) by A115;
reconsider S = T . i as Division of ['a,b'] by INTEGRA1:def 3;
A124: k in dom S1 by A121, A122, A123, FINSEQ_1:def 3;
len S = (len S1) + (len S2) by A123, FINSEQ_1:35;
then len S1 <= len S by NAT_1:11;
then Seg (len S1) c= Seg (len S) by FINSEQ_1:7;
then k in Seg (len S) by A121, A122, A123;
then A125: k in dom S by FINSEQ_1:def 3;
A126: ( divset (T . i),k = [.(inf (divset (T . i),k)),(sup (divset (T . i),k)).] & divset (T1 . i),k = [.(inf (divset (T1 . i),k)),(sup (divset (T1 . i),k)).] ) by INTEGRA1:5;

A127: now

assume A128: k = 1 ; :: thesis:
hence divset (T . i),k = [.(inf ['a,b']),(sup (divset (T . i),k)).] by A125, A126, INTEGRA1:def 5
.= [.(inf ['a,b']),(S . k).] by A125, A128, INTEGRA1:def 5
.= [.(inf ['a,b']),(S1 . k).] by A123, A124, FINSEQ_1:def 7
.= [.(inf (divset (T1 . i),k)),(S1 . 1).] by A6, A123, A124, A128, INTEGRA1:def 5
.= divset (T1 . i),k by A123, A124, A126, A128, INTEGRA1:def 5 ;
:: thesis:

end;

now

assume A129: k <> 1 ; :: thesis:
A130: ( 1 <= k & k <= len S1 ) by A121, A122, A123, FINSEQ_1:3;
k - 1 <= k - 0 by XREAL_1:12;
then A131: k - 1 <= len S1 by A130, XXREAL_0:2;
A132: 1 < k by A129, A130, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A133: 2 - 1 <= k - 1 by XREAL_1:11;
k - 1 is Element of NAT by A132, NAT_1:20;
then k - 1 in Seg (len S1) by A131, A133;
then A135: k - 1 in dom S1 by FINSEQ_1:def 3;
thus divset (T . i),k = [.(S . (k - 1)),(sup (divset (T . i),k)).] by A125, A126, A129, INTEGRA1:def 5
.= [.(S . (k - 1)),(S . k).] by A125, A129, INTEGRA1:def 5
.= [.(S . (k - 1)),(S1 . k).] by A123, A124, FINSEQ_1:def 7
.= [.(S1 . (k - 1)),(S1 . k).] by A123, A135, FINSEQ_1:def 7
.= [.(inf (divset (T1 . i),k)),(S1 . k).] by A123, A124, A129, INTEGRA1:def 5
.= divset (T1 . i),k by A123, A124, A126, A129, INTEGRA1:def 5 ; :: thesis:

end;

hence divset (T . i),k = divset (T1 . i),k by A127; :: thesis:

end;

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

let i, k be Element of NAT ; :: thesis:
let S01 be Division of ['a,c']; :: thesis:
let S02 be Division of ['c,b']; :: thesis:
assume A137: ( S01 = T1 . i & S02 = T2 . i ) ; :: thesis:
assume A138: k in Seg (len S02) ; :: thesis:
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A139: ( S1 = T1 . i & S2 = T2 . i & T . i = S1 ^ S2 ) by A115;
reconsider S = T . i as Division of ['a,b'] by INTEGRA1:def 3;
A140: k in dom S2 by A137, A138, A139, FINSEQ_1:def 3;
then A141: (len S1) + k in dom S by A139, FINSEQ_1:41;
A142: ( divset (T . i),((len S1) + k) = [.(inf (divset (T . i),((len S1) + k))),(sup (divset (T . i),((len S1) + k))).] & divset (T2 . i),k = [.(inf (divset (T2 . i),k)),(sup (divset (T2 . i),k)).] ) by INTEGRA1:5;

A143: now

assume A144: k = 1 ; :: thesis:
len S1 <> 0 ;
then A145: (len S1) + k <> 1 by A144;
len S1 in Seg (len S1) by FINSEQ_1:5;
then A146: len S1 in dom S1 by FINSEQ_1:def 3;
thus divset (T . i),((len S1) + k) = [.(S . (((len S1) + k) - 1)),(sup (divset (T . i),((len S1) + k))).] by A141, A142, A145, INTEGRA1:def 5
.= [.(S1 . (len S1)),(sup (divset (T . i),((len S1) + k))).] by A139, A144, A146, FINSEQ_1:def 7
.= [.(sup ['a,c']),(sup (divset (T . i),((len S1) + k))).] by INTEGRA1:def 2
.= [.(inf ['c,b']),(S . ((len S1) + k)).] by A6, A141, A145, INTEGRA1:def 5
.= [.(inf ['c,b']),(S2 . k).] by A139, A140, FINSEQ_1:def 7
.= [.(inf (divset (T2 . i),k)),(S2 . 1).] by A139, A140, A144, INTEGRA1:def 5
.= divset (T2 . i),k by A139, A140, A142, A144, INTEGRA1:def 5 ; :: thesis:

end;

now

assume A147: k <> 1 ; :: thesis:
A148: ( 1 <= k & k <= len S2 ) by A137, A138, A139, FINSEQ_1:3;
then A149: 1 < k by A147, XXREAL_0:1;
then A150: 1 + 0 < k + (len S1) by XREAL_1:10;
k - 1 <= k - 0 by XREAL_1:12;
then A151: k - 1 <= len S2 by A148, XXREAL_0:2;
1 + 1 <= k by A149, NAT_1:13;
then A152: 2 - 1 <= k - 1 by XREAL_1:11;
k - 1 is Element of NAT by A149, NAT_1:20;
then k - 1 in Seg (len S2) by A151, A152;
then A154: k - 1 in dom S2 by FINSEQ_1:def 3;
thus divset (T . i),((len S1) + k) = [.(S . (((len S1) + k) - 1)),(sup (divset (T . i),((len S1) + k))).] by A141, A142, A150, INTEGRA1:def 5
.= [.(S . (((len S1) + k) - 1)),(S . ((len S1) + k)).] by A141, A150, INTEGRA1:def 5
.= [.(S . ((len S1) + (k - 1))),(S2 . k).] by A139, A140, FINSEQ_1:def 7
.= [.(S2 . (k - 1)),(S2 . k).] by A139, A154, FINSEQ_1:def 7
.= [.(inf (divset (T2 . i),k)),(S2 . k).] by A139, A140, A147, INTEGRA1:def 5
.= divset (T2 . i),k by A139, A140, A142, A147, INTEGRA1:def 5 ; :: thesis:

end;

hence divset (T . i),((len S01) + k) = divset (T2 . i),k by A137, A139, A143; :: thesis:

end;

set XAC = chi ['a,c'],['a,c'];
set XAB = chi ['a,b'],['a,b'];
A155: ( delta T is convergent & lim (delta T) = 0 )

proof

A156: now

let e be real number ; :: thesis:
assume A157: 0 < e ; :: thesis:
then consider n1 being Element of NAT such that
A158: for m being Element of NAT st n1 <= m holds
abs (((delta T1) . m) - 0 ) < e by A11, SEQ_2:def 7;
consider n2 being Element of NAT such that
A159: for m being Element of NAT st n2 <= m holds
abs (((delta T2) . m) - 0 ) < e by A50, A157, SEQ_2:def 7;
reconsider n = max n1,n2 as Element of NAT by XXREAL_0:16;
take n = n; :: thesis:

now

let m be Element of NAT ; :: thesis:
assume A160: n <= m ; :: thesis:
n1 <= n by XXREAL_0:25;
then n1 <= m by A160, XXREAL_0:2;
then abs (((delta T1) . m) - 0 ) < e by A158;
then A161: abs (delta (T1 . m)) < e by INTEGRA2:def 3;
0 <= delta (T1 . m) by INTEGRA3:8;
then A162: max (rng (upper_volume (chi ['a,c'],['a,c']),(T1 . m))) < e by A161, ABSVALUE:def 1;
n2 <= n by XXREAL_0:25;
then n2 <= m by A160, XXREAL_0:2;
then abs (((delta T2) . m) - 0 ) < e by A159;
then A163: abs (delta (T2 . m)) < e by INTEGRA2:def 3;
0 <= delta (T2 . m) by INTEGRA3:8;
then A164: max (rng (upper_volume (chi ['c,b'],['c,b']),(T2 . m))) < e by A163, ABSVALUE:def 1;
A165: for r being real number st r in rng (upper_volume (chi ['a,b'],['a,b']),(T . m)) holds
r < e

proof

let y be real number ; :: thesis:
assume y in rng (upper_volume (chi ['a,b'],['a,b']),(T . m)) ; :: thesis:
then consider x being set such that
A166: ( x in dom (upper_volume (chi ['a,b'],['a,b']),(T . m)) & y = (upper_volume (chi ['a,b'],['a,b']),(T . m)) . x ) by FUNCT_1:def 5;
A167: x in Seg (len (upper_volume (chi ['a,b'],['a,b']),(T . m))) by A166, FINSEQ_1:def 3;
reconsider i = x as Element of NAT by A166;
reconsider Tm = T . m as Division of ['a,b'] by INTEGRA1:def 3;
A168: len (upper_volume (chi ['a,b'],['a,b']),(T . m)) = len Tm by INTEGRA1:def 7;
then dom (upper_volume (chi ['a,b'],['a,b']),(T . m)) = dom Tm by FINSEQ_3:31;
then A169: y = (sup (rng ((chi ['a,b'],['a,b']) | (divset (T . m),i)))) * (vol (divset (T . m),i)) by A166, INTEGRA1:def 7;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A170: ( S1 = T1 . m & S2 = T2 . m & T . m = S1 ^ S2 ) by A115;
A171: len Tm = (len S1) + (len S2) by A170, FINSEQ_1:35;
A172: ( 1 <= i & i <= len Tm ) by A167, A168, FINSEQ_1:3;

per cases ;

suppose i <= len S1 ; :: thesis:

then A173: i in Seg (len S1) by A172;
then B173: i in dom S1 by FINSEQ_1:def 3;
A174: divset (T1 . m),i = divset (T . m),i by A120, A170, A173;
A175: divset (T1 . m),i c= ['a,c'] by A116, A170, A173;
then divset (T1 . m),i c= ['a,b'] by A5, XBOOLE_1:1;
then (chi ['a,c'],['a,c']) | (divset (T1 . m),i) = (chi ['a,b'],['a,b']) | (divset (T . m),i) by A174, A175, Th4;
then A176: y = (upper_volume (chi ['a,c'],['a,c']),(T1 . m)) . i by A169, A170, A174, B173, INTEGRA1:def 7;
len (upper_volume (chi ['a,c'],['a,c']),(T1 . m)) = len S1 by A170, INTEGRA1:def 7;
then i in dom (upper_volume (chi ['a,c'],['a,c']),(T1 . m)) by A173, FINSEQ_1:def 3;
then y in rng (upper_volume (chi ['a,c'],['a,c']),(T1 . m)) by A176, FUNCT_1:def 5;
then y <= max (rng (upper_volume (chi ['a,c'],['a,c']),(T1 . m))) by XXREAL_2:def 8;
hence y < e by A162, XXREAL_0:2; :: thesis:

end;

suppose i > len S1 ; :: thesis:

then A177: (len S1) + 1 <= i by NAT_1:13;
then consider k being Nat such that
A178: ((len S1) + 1) + k = i by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
1 + k = i - (len S1) by A178;
then A179: 1 <= 1 + k by A177, XREAL_1:21;
set i1 = 1 + k;
i - (len S1) <= len S2 by A171, A172, XREAL_1:22;
then A180: 1 + k in Seg (len S2) by A178, A179;
then B180: 1 + k in dom S2 by FINSEQ_1:def 3;
A181: divset (T2 . m),(1 + k) = divset (T . m),((len S1) + (1 + k)) by A136, A170, A180;
A182: divset (T2 . m),(1 + k) c= ['c,b'] by A118, A170, A180;
then divset (T2 . m),(1 + k) c= ['a,b'] by A5, XBOOLE_1:1;
then y = (sup (rng ((chi ['c,b'],['c,b']) | (divset (T2 . m),(1 + k))))) * (vol (divset (T2 . m),(1 + k))) by A169, A178, A181, A182, Th4;
then A183: y = (upper_volume (chi ['c,b'],['c,b']),(T2 . m)) . (1 + k) by A170, B180, INTEGRA1:def 7;
len (upper_volume (chi ['c,b'],['c,b']),(T2 . m)) = len S2 by A170, INTEGRA1:def 7;
then 1 + k in dom (upper_volume (chi ['c,b'],['c,b']),(T2 . m)) by A180, FINSEQ_1:def 3;
then y in rng (upper_volume (chi ['c,b'],['c,b']),(T2 . m)) by A183, FUNCT_1:def 5;
then y <= max (rng (upper_volume (chi ['c,b'],['c,b']),(T2 . m))) by XXREAL_2:def 8;
hence y < e by A164, XXREAL_0:2; :: thesis:

end;

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 A184: delta (T . m) < e by A165;
0 <= delta (T . m) by INTEGRA3:8;
then abs (delta (T . m)) < e by A184, ABSVALUE:def 1;
hence abs (((delta T) . m) - 0 ) < e by INTEGRA2:def 3; :: thesis:

end;

hence for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0 ) < e ; :: thesis:

end;

hence delta T is convergent by SEQ_2:def 6; :: thesis:
hence lim (delta T) = 0 by A156, SEQ_2:def 7; :: thesis:

end;

A185: (upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b'])

proof

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

proof

let i be Element of NAT ; :: thesis:
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 ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A187: ( S1 = T1 . i & S2 = T2 . i & T . i = S1 ^ S2 ) by A115;
reconsider S = T . i as Division of ['a,b'] by INTEGRA1:def 3;
A188: len F = len S by INTEGRA1:def 7
.= (len S1) + (len S2) by A187, FINSEQ_1:35
.= (len F1) + (len S2) by A187, INTEGRA1:def 7
.= (len F1) + (len F2) by A187, INTEGRA1:def 7 ;
then A189: dom F = Seg ((len F1) + (len F2)) by FINSEQ_1:def 3;

A190: now

let k be Nat; :: thesis:
len F1 <= len F by A188, NAT_1:11;
then A191: Seg (len F1) c= Seg (len F) by FINSEQ_1:7;
assume k in dom F1 ; :: thesis:
then k in Seg (len F1) by FINSEQ_1:def 3;
then A192: ( k in Seg (len F) & k in Seg (len S1) ) by A187, A191, INTEGRA1:def 7;
then k in Seg (len S) by INTEGRA1:def 7;
then k in dom S by FINSEQ_1:def 3;
then A193: F . k = (sup (rng ((f || ['a,b']) | (divset (T . i),k)))) * (vol (divset (T . i),k)) by INTEGRA1:def 7;
B192: k in dom S1 by A192, FINSEQ_1:def 3;
A194: divset (T . i),k = divset (T1 . i),k by A120, A187, A192;
then A195: divset (T . i),k c= ['a,c'] by A116, A187, A192;
then divset (T . i),k c= ['a,b'] by A5, XBOOLE_1:1;
then F . k = (sup (rng ((f || ['a,c']) | (divset (T1 . i),k)))) * (vol (divset (T1 . i),k)) by A193, A194, A195, Th3;
hence F . k = F1 . k by A187, B192, INTEGRA1:def 7; :: thesis:

end;

now

let k be Nat; :: thesis:
assume A196: k in dom F2 ; :: thesis:
then k in Seg (len F2) by FINSEQ_1:def 3;
then A197: ( 1 <= k & k <= len F2 ) by FINSEQ_1:3;
then A198: (len F1) + k <= len F by A188, XREAL_1:8;
A199: 1 + (len F1) <= k + (len F1) by A197, XREAL_1:8;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by A199, XXREAL_0:2;
then A200: k + (len F1) in Seg (len F) by A198;
k in Seg (len F2) by A196, FINSEQ_1:def 3;
then A201: k in Seg (len S2) by A187, INTEGRA1:def 7;
then B201: k in dom S2 by FINSEQ_1:def 3;
A202: len F1 = len S1 by A187, INTEGRA1:def 7;
(len F1) + k in Seg (len S) by A200, INTEGRA1:def 7;
then (len F1) + k in dom S by FINSEQ_1:def 3;
then A203: F . ((len F1) + k) = (sup (rng ((f || ['a,b']) | (divset (T . i),((len F1) + k))))) * (vol (divset (T . i),((len F1) + k))) by INTEGRA1:def 7;
A204: divset (T . i),((len F1) + k) = divset (T2 . i),k by A136, A187, A201, A202;
then A205: divset (T . i),((len F1) + k) c= ['c,b'] by A118, A187, A201;
then divset (T . i),((len F1) + k) c= ['a,b'] by A5, XBOOLE_1:1;
then F . ((len F1) + k) = (sup (rng ((f || ['c,b']) | (divset (T2 . i),k)))) * (vol (divset (T2 . i),k)) by A203, A204, A205, Th3;
hence F . ((len F1) + k) = F2 . k by A187, B201, INTEGRA1:def 7; :: thesis:

end;

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

end;

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

proof

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)) by A186;
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:105; :: thesis:

end;

now

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

end;

then A207: upper_sum (f || ['a,b']),T = (upper_sum (f || ['a,c']),T1) + (upper_sum (f || ['c,b']),T2) by SEQ_1:11;
A208: ( upper_sum (f || ['a,c']),T1 is convergent & lim (upper_sum (f || ['a,c']),T1) = upper_integral (f || ['a,c']) & upper_sum (f || ['c,b']),T2 is convergent & lim (upper_sum (f || ['c,b']),T2) = upper_integral (f || ['c,b']) ) by A7, A10, A11, A50, INTEGRA4:9;
(f || ['a,b']) | ['a,b'] is bounded by A1, INTEGRA5:9;
then upper_integral (f || ['a,b']) = lim (upper_sum (f || ['a,b']),T) by A7, A155, INTEGRA4:9;
hence (upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b']) by A207, A208, SEQ_2:20; :: thesis:

end;

A209: integral f,a,b = integral f,['a,b'] by A1, INTEGRA5:def 5
.= (integral (f || ['a,c'])) + (integral (f || ['c,b'])) by A185 ;
A210: integral f,a,c = integral f,['a,c'] by A3, INTEGRA5:def 5;
integral f,c,b = integral f,['c,b'] by A3, INTEGRA5:def 5
.= integral (f || ['c,b']) ;
hence integral f,a,b = (integral f,a,c) + (integral f,c,b) by A209, A210; :: thesis:
A211: (lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b'])

proof

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

let i be Element of NAT ; :: thesis:
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 ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A213: ( S1 = T1 . i & S2 = T2 . i & T . i = S1 ^ S2 ) by A115;
reconsider S = T . i as Division of ['a,b'] by INTEGRA1:def 3;
A214: len F = len S by INTEGRA1:def 8
.= (len S1) + (len S2) by A213, FINSEQ_1:35
.= (len F1) + (len S2) by A213, INTEGRA1:def 8 ;
then A215: len F = (len F1) + (len F2) by A213, INTEGRA1:def 8;
then A216: dom F = Seg ((len F1) + (len F2)) by FINSEQ_1:def 3;

A217: now

let k be Nat; :: thesis:
assume A218: k in dom F1 ; :: thesis:
T: len F1 <= len F by A214, NAT_1:11;
B219: dom F1 c= dom F by T, FINSEQ_3:32;
k in Seg (len F1) by A218, FINSEQ_1:def 3;
then A221: k in Seg (len S1) by A213, INTEGRA1:def 8;
then B221: k in dom S1 by FINSEQ_1:def 3;
len (lower_volume (f || ['a,b']),(T . i)) = len S by INTEGRA1:def 8;
then dom (lower_volume (f || ['a,b']),(T . i)) = dom S by FINSEQ_3:31;
then A222: F . k = (inf (rng ((f || ['a,b']) | (divset (T . i),k)))) * (vol (divset (T . i),k)) by A218, B219, INTEGRA1:def 8;
A223: ( divset (T . i),k = divset (T1 . i),k & divset (T1 . i),k c= ['a,c'] ) by A116, A120, A213, A221;
then divset (T . i),k c= ['a,b'] by A5, XBOOLE_1:1;
then F . k = (inf (rng ((f || ['a,c']) | (divset (T1 . i),k)))) * (vol (divset (T1 . i),k)) by A222, A223, Th3;
hence F . k = F1 . k by A213, B221, INTEGRA1:def 8; :: thesis:

end;

now

let k be Nat; :: thesis:
assume k in dom F2 ; :: thesis:
then A224: k in Seg (len F2) by FINSEQ_1:def 3;
then A225: ( 1 <= k & k <= len F2 ) by FINSEQ_1:3;
then A226: (len F1) + k <= len F by A215, XREAL_1:8;
A227: 1 + (len F1) <= k + (len F1) by A225, XREAL_1:8;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by A227, XXREAL_0:2;
then k + (len F1) in Seg (len F) by A226;
then (len F1) + k in Seg (len S) by INTEGRA1:def 8;
then (len F1) + k in dom S by FINSEQ_1:def 3;
then A228: F . ((len F1) + k) = (inf (rng ((f || ['a,b']) | (divset (T . i),((len F1) + k))))) * (vol (divset (T . i),((len F1) + k))) by INTEGRA1:def 8;
A229: ( k in Seg (len S2) & len F1 = len S1 ) by A213, A224, INTEGRA1:def 8;
then B229: k in dom S2 by FINSEQ_1:def 3;
A230: ( divset (T . i),((len F1) + k) = divset (T2 . i),k & divset (T2 . i),k c= ['c,b'] ) by A118, A136, A213, A229;
then divset (T . i),((len F1) + k) c= ['a,b'] by A5, XBOOLE_1:1;
then F . ((len F1) + k) = (inf (rng ((f || ['c,b']) | (divset (T2 . i),k)))) * (vol (divset (T2 . i),k)) by A228, A230, Th3;
hence F . ((len F1) + k) = F2 . k by A213, B229, INTEGRA1:def 8; :: thesis:

end;

hence lower_volume (f || ['a,b']),(T . i) = (lower_volume (f || ['a,c']),(T1 . i)) ^ (lower_volume (f || ['c,b']),(T2 . i)) by A216, A217, FINSEQ_1:def 7; :: thesis:

end;

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

proof

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)) by A212;
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:105; :: thesis:

end;

now

let i be Element of NAT ; :: thesis:
thus (lower_sum (f || ['a,b']),T) . i = lower_sum (f || ['a,b']),(T . i) by INTEGRA2:def 5
.= (lower_sum (f || ['a,c']),(T1 . i)) + (Sum (lower_volume (f || ['c,b']),(T2 . i))) by A231
.= ((lower_sum (f || ['a,c']),T1) . i) + (lower_sum (f || ['c,b']),(T2 . i)) by INTEGRA2:def 5
.= ((lower_sum (f || ['a,c']),T1) . i) + ((lower_sum (f || ['c,b']),T2) . i) by INTEGRA2:def 5 ; :: thesis:

end;

then A232: lower_sum (f || ['a,b']),T = (lower_sum (f || ['a,c']),T1) + (lower_sum (f || ['c,b']),T2) by SEQ_1:11;
A233: ( lower_sum (f || ['a,c']),T1 is convergent & lim (lower_sum (f || ['a,c']),T1) = lower_integral (f || ['a,c']) & lower_sum (f || ['c,b']),T2 is convergent & lim (lower_sum (f || ['c,b']),T2) = lower_integral (f || ['c,b']) ) by A7, A10, A11, A50, INTEGRA4:8;
(f || ['a,b']) | ['a,b'] is bounded by A1, INTEGRA5:9;
then lower_integral (f || ['a,b']) = lim (lower_sum (f || ['a,b']),T) by A7, A155, INTEGRA4:8;
hence (lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b']) by A232, A233, SEQ_2:20; :: thesis:

end;