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, INTEGRA1:def 10;
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
then A10: D1 in dom (upper_sum_set f) by XBOOLE_0:def 4;
then (upper_sum_set f) /. D1 = (upper_sum_set f) . D1 by PARTFUN1:def 6
.= upper_sum (f,D2) by A10, FUNCT_2:def 1, INTEGRA1:def 10
.= Sum (upper_volume (f,D2)) by INTEGRA1:def 8 ;
hence (upper_sum_set f) /. D1 = 0 by A9, FINSOP_1:11; :: thesis: verum

end;

then (upper_sum_set f) | (divs A) is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A11: rng ((upper_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:37;
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) and
A14: (upper_sum_set f) . D1 = x1 by PARTFUN1:3;
D1 in (divs A) /\ (dom (upper_sum_set f)) by A13, XBOOLE_1:28;
then A15: D1 in dom ((upper_sum_set f) | (divs A)) by RELAT_1:61;
then ((upper_sum_set f) | (divs A)) . D1 = (upper_sum_set f) . D1 by FUNCT_1:47;
hence x1 in rng ((upper_sum_set f) | (divs A)) by A14, A15, FUNCT_1:def 3; :: 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;

hence f is upper_integrable by A11, 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 A16: the Element of divs A in dom (upper_sum_set f) by FUNCT_2:def 1, INTEGRA1:def 10;
then A17: (upper_sum_set f) . the Element of divs A in rng (upper_sum_set f) by FUNCT_1:def 3;
A18: (upper_sum_set f) . the Element of divs A = (upper_sum_set f) /. the Element of divs A by A16, PARTFUN1:def 6;
the Element of divs A in (divs A) /\ (dom (upper_sum_set f)) by A16, XBOOLE_0:def 4;
hence 0 in rng (upper_sum_set f) by A3, A17, A18; :: thesis: verum

end;

then A19: x = 0 by A11, A12, TARSKI:def 1;
rng ((upper_sum_set f) | (divs A)) c= rng (upper_sum_set f) by RELAT_1:70;
then rng (upper_sum_set f) = {x} by A11, A12, XBOOLE_0:def 10;
then lower_bound (rng (upper_sum_set f)) = 0 by A19, SEQ_4:9;
hence upper_integral f = 0 by INTEGRA1:def 14; :: thesis: verum