let A be 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 INTEGRA1:def 12;
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 = 0

proof

let D1 be Element of divs A; :: thesis: ( D1 in (divs A) /\ (dom (lower_sum_set f)) implies (lower_sum_set f) /. D1 = 0 )
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
A4: len (lower_volume (f,D2)) = len D2 by INTEGRA1:def 8
.= 1 by A2, Th1 ;
A5: len D2 = 1 by A2, Th1;
then 1 in Seg (len D2) by FINSEQ_1:3;
then A6: 1 in dom D2 by FINSEQ_1:def 3;
rng D2 <> {} ;
then A7: 1 in dom D2 by FINSEQ_3:34;
then A8: upper_bound (divset (D2,(len D2))) = D2 . (len D2) by A5, INTEGRA1:def 5
.= 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:5
.= [.(lower_bound A),(upper_bound A).] by A5, A7, A8, INTEGRA1:def 5 ;
then divset (D2,1) = A by INTEGRA1:5;
then (lower_volume (f,D2)) . 1 = (lower_bound (rng (f | (divset (D2,1))))) * (vol A) by A6, INTEGRA1:def 8
.= 0 by A2 ;
then A9: lower_volume (f,D2) = <*0*> by A4, FINSEQ_1:57;
assume D1 in (divs A) /\ (dom (lower_sum_set f)) ; :: thesis: (lower_sum_set f) /. D1 = 0
then A10: D1 in dom (lower_sum_set f) by XBOOLE_0:def 4;
then (lower_sum_set f) /. D1 = (lower_sum_set f) . D1 by PARTFUN1:def 8
.= lower_sum (f,D2) by A10, INTEGRA1:def 12
.= Sum (lower_volume (f,D2)) by INTEGRA1:def 10 ;
hence (lower_sum_set f) /. D1 = 0 by A9, FINSOP_1:12; :: thesis: verum

end;

then (lower_sum_set f) | (divs A) is constant by PARTFUN2:54;
then consider x being Element of REAL such that
A11: rng ((lower_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:56;
A12: rng (lower_sum_set f) c= rng ((lower_sum_set f) | (divs A))

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng (lower_sum_set f) or x1 in rng ((lower_sum_set f) | (divs A)) )
( x1 in rng (lower_sum_set f) implies x1 in rng ((lower_sum_set f) | (divs A)) )

proof

assume x1 in rng (lower_sum_set f) ; :: thesis: x1 in rng ((lower_sum_set f) | (divs A))
then consider D1 being Element of divs A such that
A13: D1 in dom (lower_sum_set f) and
A14: (lower_sum_set f) . D1 = x1 by PARTFUN1:26;
D1 in (divs A) /\ (dom (lower_sum_set f)) by A13, XBOOLE_1:28;
then A15: D1 in dom ((lower_sum_set f) | (divs A)) by RELAT_1:90;
then ((lower_sum_set f) | (divs A)) . D1 = (lower_sum_set f) . D1 by FUNCT_1:70;
hence x1 in rng ((lower_sum_set f) | (divs A)) by A14, A15, FUNCT_1:def 5; :: thesis: verum

end;

hence ( not x1 in rng (lower_sum_set f) or x1 in rng ((lower_sum_set f) | (divs A)) ) ; :: thesis: verum

end;

hence f is lower_integrable by A11, INTEGRA1:def 14; :: thesis: lower_integral f = 0
0 in rng (lower_sum_set f)

proof

consider D1 being Element of divs A;
D1 in divs A ;
then A16: D1 in dom (lower_sum_set f) by INTEGRA1:def 12;
then A17: (lower_sum_set f) . D1 in rng (lower_sum_set f) by FUNCT_1:def 5;
A18: (lower_sum_set f) . D1 = (lower_sum_set f) /. D1 by A16, PARTFUN1:def 8;
D1 in (divs A) /\ (dom (lower_sum_set f)) by A16, XBOOLE_0:def 4;
hence 0 in rng (lower_sum_set f) by A3, A17, A18; :: thesis: verum

end;

then A19: x = 0 by A11, A12, TARSKI:def 1;
rng ((lower_sum_set f) | (divs A)) c= rng (lower_sum_set f) by RELAT_1:99;
then rng (lower_sum_set f) = {x} by A11, A12, XBOOLE_0:def 10;
then upper_bound (rng (lower_sum_set f)) = 0 by A19, SEQ_4:22;
hence lower_integral f = 0 by INTEGRA1:def 16; :: thesis: verum