let A be non empty 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 :: thesis:

per cases ;

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

for n being Nat holds (delta T) . n <> 0

proof

let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider D = T . nn as Division of A ;
assume (delta T) . n = 0 ; :: thesis:
then delta (T . nn) = 0 by INTEGRA3:def 2;
then A5: max (rng (upper_volume ((chi (A,A)),(T . nn)))) = 0 by INTEGRA3:def 1;
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 6;
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 3;
then (upper_volume ((chi (A,A)),D)) . k <= 0 by A5, XXREAL_2:def 8;
then vol (divset (D,k)) <= 0 by A7, INTEGRA1:20;
hence vol (divset (D,k)) = 0 by INTEGRA1:9; :: 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:1;
then A11: j in Seg (len D) by INTEGRA1:def 6;
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:20;
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:7; :: thesis:

end;

len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def 6;
then len (upper_volume ((chi (A,A)),D)) = len ((len D) |-> 0) by CARD_1:def 7;
then upper_volume ((chi (A,A)),D) = (len D) |-> 0 by A8, FINSEQ_1:14;
then Sum (upper_volume ((chi (A,A)),D)) = 0 by RVSUM_1:81;
hence contradiction by A4, INTEGRA1:24; :: thesis:

end;

then delta T is non-zero by SEQ_1:5;
then ( delta T is 0 -convergent & delta T is non-zero ) by A2, A3, FDIFF_1:def 1;
hence ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) by A1, A4, INTEGRA3:26; :: thesis:

end;

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

A14: for n being Nat holds (upper_sum (f,T)) . n = In (0,REAL)

proof

let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider D = T . nn as Division of A ;
A15: len D = 1 by A13, Th1;
then A16: len (upper_volume (f,D)) = 1 by INTEGRA1:def 6;
rng D <> {} ;
then A17: 1 in dom D by FINSEQ_3:32;
then A18: upper_bound (divset (D,(len D))) = D . (len D) by A15, INTEGRA1:def 4
.= upper_bound A by INTEGRA1:def 2 ;
1 in Seg (len D) by A15, FINSEQ_1:1;
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:4
.= [.(lower_bound A),(upper_bound A).] by A15, A17, A18, INTEGRA1:def 4 ;
then divset (D,1) = A by INTEGRA1:4;
then (upper_volume (f,D)) . 1 = (upper_bound (rng (f | (divset (D,1))))) * (vol A) by A19, INTEGRA1:def 6
.= 0 by A13 ;
then upper_volume (f,D) = <*0*> by A16, FINSEQ_1:40;
then Sum (upper_volume (f,D)) = In (0,REAL) by FINSOP_1:11;
then upper_sum (f,D) = 0 by INTEGRA1:def 8;
hence (upper_sum (f,T)) . n = In (0,REAL) by INTEGRA2:def 2; :: thesis:

end;

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

end;

end;

end;

hence ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) ; :: thesis: