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 lower_integrable & lower_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 lower_integrable & lower_integral f = 0 )
let D be Element of divs A; :: thesis: ( vol A = 0 implies ( f is lower_integrable & lower_integral f = 0 ) )
(divs A) /\ (dom (lower_sum_set f)) = (divs A) /\ (divs A) by FUNCT_2:def 1;
then A1: divs A meets dom (lower_sum_set f) by XBOOLE_0:def 7;
assume A2: vol A = 0 ; :: thesis: ( f is lower_integrable & lower_integral f = 0 )
A3: for D1 being Element of divs A st D1 in (divs A) /\ (dom (lower_sum_set f)) holds
(lower_sum_set f) /. D1 = In (0,REAL)

proof

let D1 be Element of divs A; :: thesis: ( D1 in (divs A) /\ (dom (lower_sum_set f)) implies (lower_sum_set f) /. D1 = In (0,REAL) )
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
A4: len (lower_volume (f,D2)) = len D2 by INTEGRA1:def 7
.= 1 by A2, Th1 ;
A5: len D2 = 1 by A2, Th1;
then 1 in Seg (len D2) by FINSEQ_1:1;
then A6: 1 in dom D2 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 (lower_volume (f,D2)) . 1 = (lower_bound (rng (f | (divset (D2,1))))) * (vol A) by A6, INTEGRA1:def 7
.= 0 by A2 ;
then A9: lower_volume (f,D2) = <*(In (0,REAL))*> by A4, FINSEQ_1:40;
assume D1 in (divs A) /\ (dom (lower_sum_set f)) ; :: thesis: (lower_sum_set f) /. D1 = In (0,REAL)
(lower_sum_set f) /. D1 = (lower_sum_set f) . D1
.= lower_sum (f,D2) by INTEGRA1:def 11
.= Sum (lower_volume (f,D2)) by INTEGRA1:def 9 ;
hence (lower_sum_set f) /. D1 = In (0,REAL) by A9, FINSOP_1:11; :: thesis: verum

end;

then (lower_sum_set f) | (divs A) is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A10: rng ((lower_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:37;
thus f is lower_integrable by A10, INTEGRA1:def 13; :: thesis: lower_integral f = 0
0 in rng (lower_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 (lower_sum_set f) by FUNCT_2:def 1;
then A12: (lower_sum_set f) . the Element of divs A in rng (lower_sum_set f) by FUNCT_1:def 3;
A13: (lower_sum_set f) . the Element of divs A = (lower_sum_set f) /. the Element of divs A ;
the Element of divs A in (divs A) /\ (dom (lower_sum_set f)) by A11, XBOOLE_0:def 4;
hence 0 in rng (lower_sum_set f) by A3, A12, A13; :: thesis: verum

end;

then A14: x = 0 by A10, TARSKI:def 1;
rng (lower_sum_set f) = {x} by A10;
then upper_bound (rng (lower_sum_set f)) = 0 by A14, SEQ_4:9;
hence lower_integral f = 0 by INTEGRA1:def 15; :: thesis: verum