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 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 ) )
assume A1: vol A = 0 ; :: thesis: ( f is upper_integrable & upper_integral f = 0 )
(divs A) /\ (dom (upper_sum_set f)) = (divs A) /\ (divs A) by INTEGRA1:def 11;
then A2: divs A meets dom (upper_sum_set f) by XBOOLE_0:def 7;
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 )
assume D1 in (divs A) /\ (dom (upper_sum_set f)) ; :: thesis: (upper_sum_set f) /. D1 = 0
then A4: D1 in dom (upper_sum_set f) by XBOOLE_0:def 4;
then A5: (upper_sum_set f) /. D1 = (upper_sum_set f) . D1 by PARTFUN1:def 8
.= upper_sum f,D1 by A4, INTEGRA1:def 11
.= Sum (upper_volume f,D1) by INTEGRA1:def 9 ;
upper_volume f,D1 = <*0 *>

proof

A6: len (upper_volume f,D1) = len D1 by INTEGRA1:def 7
.= 1 by A1, Th1 ;
rng D1 <> {} ;
then A7: ( len D1 = 1 & 1 in dom D1 ) by A1, Th1, FINSEQ_3:34;
A8: divset D1,1 = A

proof

A9: upper_bound (divset D1,(len D1)) = D1 . (len D1) by A7, INTEGRA1:def 5
.= upper_bound A by INTEGRA1:def 2 ;
divset D1,1 = [.(lower_bound (divset D1,(len D1))),(upper_bound (divset D1,(len D1))).] by A7, INTEGRA1:5
.= [.(lower_bound A),(upper_bound A).] by A7, A9, INTEGRA1:def 5 ;
hence divset D1,1 = A by INTEGRA1:5; :: thesis: verum

end;

1 in Seg (len D1) by A7, FINSEQ_1:3;
then 1 in dom D1 by FINSEQ_1:def 3;
then (upper_volume f,D1) . 1 = (upper_bound (rng (f | (divset D1,1)))) * (vol A) by A8, INTEGRA1:def 7
.= 0 by A1 ;
hence upper_volume f,D1 = <*0 *> by A6, FINSEQ_1:57; :: thesis: verum

end;

hence (upper_sum_set f) /. D1 = 0 by A5, FINSOP_1:12; :: thesis: verum

end;

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

proof

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

proof

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

end;

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

end;

then A15: rng (upper_sum_set f) = {x} by A10, A11, XBOOLE_0:def 10;
then rng (upper_sum_set f) is bounded ;
then rng (upper_sum_set f) is bounded_below ;
hence f is upper_integrable by INTEGRA1:def 13; :: thesis: upper_integral f = 0
x = 0

proof

0 in rng (upper_sum_set f)

proof

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

end;

hence x = 0 by A10, A12, TARSKI:def 1; :: thesis: verum

end;

then lower_bound (rng (upper_sum_set f)) = 0 by A15, SEQ_4:22;
hence upper_integral f = 0 by INTEGRA1:def 15; :: thesis: verum