let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
let f be PartFunc of A,REAL; :: thesis: for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
let D be Element of divs A; :: thesis: ( vol A = 0 implies ( f is upper_integrable & upper_integral f = 0 ) )
(divs A) /\ (dom (upper_sum_set f)) = (divs A) /\ (divs A) by FUNCT_2:def 1;
then A1: divs A meets dom (upper_sum_set f) by XBOOLE_0:def 7;
assume A2: vol A = 0 ; :: thesis: ( f is upper_integrable & upper_integral f = 0 )
A3: for D1 being Element of divs A st D1 in (divs A) /\ (dom (upper_sum_set f)) holds
(upper_sum_set f) /. D1 = 0

proof

let D1 be Element of divs A; :: thesis: ( D1 in (divs A) /\ (dom (upper_sum_set f)) implies (upper_sum_set f) /. D1 = 0 )
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
A4: len (upper_volume (f,D2)) = len D2 by INTEGRA1:def 6
.= 1 by A2, Th1 ;
A5: len D2 = 1 by A2, Th1;
then 1 in Seg (len D1) by FINSEQ_1:1;
then A6: 1 in dom D1 by FINSEQ_1:def 3;
rng D2 <> {} ;
then A7: 1 in dom D2 by FINSEQ_3:32;
then A8: upper_bound (divset (D2,(len D2))) = D2 . (len D2) by A5, INTEGRA1:def 4
.= upper_bound A by INTEGRA1:def 2 ;
divset (D2,1) = [.(lower_bound (divset (D2,(len D2)))),(upper_bound (divset (D2,(len D2)))).] by A5, INTEGRA1:4
.= [.(lower_bound A),(upper_bound A).] by A5, A7, A8, INTEGRA1:def 4 ;
then divset (D2,1) = A by INTEGRA1:4;
then (upper_volume (f,D2)) . 1 = (upper_bound (rng (f | (divset (D2,1))))) * (vol A) by A6, INTEGRA1:def 6
.= 0 by A2 ;
then A9: upper_volume (f,D2) = <*0*> by A4, FINSEQ_1:40;
assume D1 in (divs A) /\ (dom (upper_sum_set f)) ; :: thesis: (upper_sum_set f) /. D1 = 0
(upper_sum_set f) /. D1 = (upper_sum_set f) . D1
.= upper_sum (f,D2) by INTEGRA1:def 10
.= Sum (upper_volume (f,D2)) by INTEGRA1:def 8 ;
hence (upper_sum_set f) /. D1 = 0 by A9, FINSOP_1:11, Lm1; :: thesis: verum

end;

then (upper_sum_set f) | (divs A) is constant by PARTFUN2:35, Lm1;
then consider x being Element of REAL such that
A10: rng ((upper_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:37;
thus f is upper_integrable by A10, INTEGRA1:def 12; :: thesis: upper_integral f = 0
0 in rng (upper_sum_set f)

proof

set D1 = the Element of divs A;
the Element of divs A in divs A ;
then A11: the Element of divs A in dom (upper_sum_set f) by FUNCT_2:def 1;
then A12: (upper_sum_set f) . the Element of divs A in rng (upper_sum_set f) by FUNCT_1:def 3;
A13: (upper_sum_set f) . the Element of divs A = (upper_sum_set f) /. the Element of divs A ;
the Element of divs A in (divs A) /\ (dom (upper_sum_set f)) by A11, XBOOLE_0:def 4;
hence 0 in rng (upper_sum_set f) by A3, A12, A13; :: thesis: verum

end;

then A14: x = 0 by A10, TARSKI:def 1;
rng (upper_sum_set f) = {x} by A10;
then lower_bound (rng (upper_sum_set f)) = 0 by A14, SEQ_4:9;
hence upper_integral f = 0 by INTEGRA1:def 14; :: thesis: verum