let A be closed-interval Subset of REAL ; :: thesis:
let f be Function of A,REAL ; :: thesis:
let T be DivSequence of A; :: thesis:
assume A1: f | A is bounded ; :: thesis:
assume A2: delta T is convergent ; :: thesis:
assume A3: lim (delta T) = 0 ; :: thesis:

now

per cases ;

suppose A4: vol A <> 0 ; :: thesis:

for n being Element of NAT holds (delta T) . n <> 0

proof

let n be Element of NAT ; :: thesis:
reconsider mm = rng (upper_volume (chi A,A),(T . n)) as non empty finite Subset of REAL ;
reconsider D = T . n as Division of A ;
assume (delta T) . n = 0 ; :: thesis:
then delta (T . n) = 0 by INTEGRA2:def 3;
then A5: max mm = 0 by INTEGRA1:def 19;
A6: for k being Element of NAT st k in dom D holds
vol (divset D,k) = 0

proof

let k be Element of NAT ; :: thesis:
assume A7: k in dom D ; :: thesis:
then k in Seg (len D) by FINSEQ_1:def 3;
then k in Seg (len (upper_volume (chi A,A),D)) by INTEGRA1:def 7;
then k in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D) . k in rng (upper_volume (chi A,A),D) by FUNCT_1:def 5;
then (upper_volume (chi A,A),D) . k <= 0 by A5, XXREAL_2:def 8;
then vol (divset D,k) <= 0 by A7, INTEGRA1:22;
hence vol (divset D,k) = 0 by INTEGRA1:11; :: thesis:

end;

A8: for j being Nat st 1 <= j & j <= len (upper_volume (chi A,A),D) holds
(upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j

proof

let j be Nat; :: thesis:
assume that
A9: 1 <= j and
A10: j <= len (upper_volume (chi A,A),D) ; :: thesis:
j in Seg (len (upper_volume (chi A,A),D)) by A9, A10, FINSEQ_1:3;
then A11: j in Seg (len D) by INTEGRA1:def 7;
then j in dom D by FINSEQ_1:def 3;
then A12: (upper_volume (chi A,A),D) . j = vol (divset D,j) by INTEGRA1:22;
j in dom D by A11, FINSEQ_1:def 3;
then (upper_volume (chi A,A),D) . j = 0 by A6, A12;
hence (upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j by A11, FUNCOP_1:13; :: thesis:

end;

len (upper_volume (chi A,A),D) = len D by INTEGRA1:def 7;
then len (upper_volume (chi A,A),D) = len ((len D) |-> 0 ) by FINSEQ_1:def 18;
then upper_volume (chi A,A),D = (len D) |-> 0 by A8, FINSEQ_1:18;
then Sum (upper_volume (chi A,A),D) = 0 by RVSUM_1:111;
hence contradiction by A4, INTEGRA1:26; :: thesis:

end;

then delta T is non-zero by SEQ_1:7;
then delta T is convergent_to_0 by A2, A3, FDIFF_1:def 1;
hence ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f ) by A1, A4, INTEGRA3:19; :: thesis:

end;

suppose A13: vol A = 0 ; :: thesis:

A14: for n being Nat holds (lower_sum f,T) . n = 0

proof

let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
reconsider D = T . nn as Division of A ;
A15: len D = 1 by A13, Th1;
then A16: len (lower_volume f,D) = 1 by INTEGRA1:def 8;
rng D <> {} ;
then A17: 1 in dom D by FINSEQ_3:34;
then A18: upper_bound (divset D,(len D)) = D . (len D) by A15, INTEGRA1:def 5
.= upper_bound A by INTEGRA1:def 2 ;
1 in Seg (len D) by A15, FINSEQ_1:3;
then A19: 1 in dom D by FINSEQ_1:def 3;
divset D,1 = [.(lower_bound (divset D,(len D))),(upper_bound (divset D,(len D))).] by A15, INTEGRA1:5
.= [.(lower_bound A),(upper_bound A).] by A15, A17, A18, INTEGRA1:def 5 ;
then divset D,1 = A by INTEGRA1:5;
then (lower_volume f,D) . 1 = (lower_bound (rng (f | (divset D,1)))) * (vol A) by A19, INTEGRA1:def 8
.= 0 by A13 ;
then lower_volume f,D = <*0 *> by A16, FINSEQ_1:57;
then Sum (lower_volume f,D) = 0 by FINSOP_1:12;
then lower_sum f,D = 0 by INTEGRA1:def 10;
hence (lower_sum f,T) . n = 0 by INTEGRA2:def 5; :: thesis:

end;

then A20: lower_sum f,T is constant by VALUED_0:def 18;
hence lower_sum f,T is convergent ; :: thesis:
(lower_sum f,T) . 1 = 0 by A14;
then lim (lower_sum f,T) = 0 by A20, SEQ_4:40;
hence lim (lower_sum f,T) = lower_integral f by A13, Lm2; :: thesis:

end;

end;

end;

hence ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f ) ; :: thesis: