let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds
( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f )
let f be Function of A,REAL ; :: thesis: for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds
( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f )
let T be DivSequence of A; :: thesis: ( f | A is bounded & delta T is convergent & lim (delta T) = 0 implies ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f ) )
assume A1: f | A is bounded ; :: thesis: ( not delta T is convergent or not lim (delta T) = 0 or ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f ) )
assume A2: delta T is convergent ; :: thesis: ( not lim (delta T) = 0 or ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f ) )
assume A3: lim (delta T) = 0 ; :: thesis: ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f )

now

per cases ( vol A <> 0 or vol A = 0 ) ;

suppose A4: vol A <> 0 ; :: thesis: ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f )

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

proof

let n be Element of NAT ; :: thesis: (delta T) . n <> 0
assume (delta T) . n = 0 ; :: thesis: contradiction
then delta (T . n) = 0 by INTEGRA2:def 3;
then A5: max (rng (upper_volume (chi A,A),(T . n))) = 0 by INTEGRA1:def 19;
reconsider D = T . n as Division of A ;
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: ( k in dom D implies vol (divset D,k) = 0 )
assume k in dom D ; :: thesis: vol (divset D,k) = 0
then A7: k in Seg (len D) by FINSEQ_1:def 3;
then B7: k in dom D by FINSEQ_1:def 3;
k in Seg (len (upper_volume (chi A,A),D)) by A7, 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 B7, INTEGRA1:22;
hence vol (divset D,k) = 0 by INTEGRA1:11; :: thesis: verum

end;

upper_volume (chi A,A),D = (len D) |-> 0

proof

len (upper_volume (chi A,A),D) = len D by INTEGRA1:def 7;
then A8: len (upper_volume (chi A,A),D) = len ((len D) |-> 0 ) by FINSEQ_1:def 18;
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: ( 1 <= j & j <= len (upper_volume (chi A,A),D) implies (upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j )
assume ( 1 <= j & j <= len (upper_volume (chi A,A),D) ) ; :: thesis: (upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j
then j in Seg (len (upper_volume (chi A,A),D)) by FINSEQ_1:3;
then A9: j in Seg (len D) by INTEGRA1:def 7;
then j in dom D by FINSEQ_1:def 3;
then A10: (upper_volume (chi A,A),D) . j = vol (divset D,j) by INTEGRA1:22;
j in dom D by A9, FINSEQ_1:def 3;
then (upper_volume (chi A,A),D) . j = 0 by A6, A10;
hence (upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j by A9, FUNCOP_1:13; :: thesis: verum

end;

hence upper_volume (chi A,A),D = (len D) |-> 0 by A8, FINSEQ_1:18; :: thesis: verum

end;

then Sum (upper_volume (chi A,A),D) = 0 by RVSUM_1:111;
hence contradiction by A4, INTEGRA1:26; :: thesis: verum

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 ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f ) by A1, A4, INTEGRA3:20; :: thesis: verum

end;

suppose A11: vol A = 0 ; :: thesis: ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f )

A12: for n being Nat holds (upper_sum f,T) . n = 0

proof

let n be Nat; :: thesis: (upper_sum f,T) . n = 0
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
reconsider D = T . nn as Division of A ;
upper_sum f,D = 0

proof

rng D <> {} ;
then A13: ( len D = 1 & 1 in dom D ) by A11, Th1, FINSEQ_3:34;
then A14: len (upper_volume f,D) = 1 by INTEGRA1:def 7;
A15: divset D,1 = A

proof

A16: upper_bound (divset D,(len D)) = D . (len D) by A13, INTEGRA1:def 5
.= upper_bound A by INTEGRA1:def 2 ;
divset D,1 = [.(lower_bound (divset D,(len D))),(upper_bound (divset D,(len D))).] by A13, INTEGRA1:5
.= [.(lower_bound A),(upper_bound A).] by A13, A16, INTEGRA1:def 5 ;
hence divset D,1 = A by INTEGRA1:5; :: thesis: verum

end;

1 in Seg (len D) by A13, FINSEQ_1:3;
then 1 in dom D by FINSEQ_1:def 3;
then (upper_volume f,D) . 1 = (upper_bound (rng (f | (divset D,1)))) * (vol A) by A15, INTEGRA1:def 7
.= 0 by A11 ;
then upper_volume f,D = <*0 *> by A14, FINSEQ_1:57;
then Sum (upper_volume f,D) = 0 by FINSOP_1:12;
hence upper_sum f,D = 0 by INTEGRA1:def 9; :: thesis: verum

end;

hence (upper_sum f,T) . n = 0 by INTEGRA2:def 4; :: thesis: verum

end;

then A17: upper_sum f,T is constant by VALUED_0:def 18;
hence upper_sum f,T is convergent ; :: thesis: lim (upper_sum f,T) = upper_integral f
(upper_sum f,T) . 1 = 0 by A12;
then lim (upper_sum f,T) = 0 by A17, SEQ_4:40;
hence lim (upper_sum f,T) = upper_integral f by A11, Lm1; :: thesis: verum

end;

end;

end;

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