let A be closed-interval Subset of REAL ; :: thesis: for D being Division of A
for f being Function of A,REAL st f | A is bounded holds
lower_sum f,D <= upper_sum f,D
let D be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded holds
lower_sum f,D <= upper_sum f,D
let f be Function of A,REAL ; :: thesis: ( f | A is bounded implies lower_sum f,D <= upper_sum f,D )
assume f | A is bounded ; :: thesis: lower_sum f,D <= upper_sum f,D
then ( f | A is bounded_below & f | A is bounded_above ) ;
then A1: ( rng f is bounded_below & rng f is bounded_above ) by Th13, Th15;
deffunc H₁( Nat) -> Element of REAL = (lower_bound (rng (f | (divset D,$1)))) * (vol (divset D,$1));
consider p being FinSequence of REAL such that
A2: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A3: dom p = dom D by A2, FINSEQ_3:31;
deffunc H₂( Nat) -> Element of REAL = (upper_bound (rng (f | (divset D,$1)))) * (vol (divset D,$1));
consider q being FinSequence of REAL such that
A4: ( len q = len D & ( for i being Nat st i in dom q holds
q . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A5: dom q = dom D by A4, FINSEQ_3:31;
A6: q = upper_volume f,D by A4, Def7, A5;
reconsider p = p as Element of (len D) -tuples_on REAL by A2, FINSEQ_2:110;
reconsider q = q as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:110;
for i being Nat st i in Seg (len D) holds
p . i <= q . i

proof

let i be Nat; :: thesis: ( i in Seg (len D) implies p . i <= q . i )
assume A7: i in Seg (len D) ; :: thesis: p . i <= q . i
then B7: i in dom D by FINSEQ_1:def 3;
A8: rng (f | (divset D,i)) is bounded_below by A1, RELAT_1:99, XXREAL_2:44;
rng (f | (divset D,i)) is bounded_above by A1, RELAT_1:99, XXREAL_2:43;
then A9: rng (f | (divset D,i)) is bounded by A8;
A10: rng (f | (divset D,i)) is non empty Subset of REAL

proof

A11: dom f = A by FUNCT_2:def 1;
i in dom D by A7, FINSEQ_1:def 3;
then dom (f | (divset D,i)) = divset D,i by A11, Th10, RELAT_1:91;
hence rng (f | (divset D,i)) is non empty Subset of REAL by RELAT_1:65; :: thesis: verum

end;

0 <= vol (divset D,i) by SEQ_4:24, XREAL_1:50;
then (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) <= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A9, A10, SEQ_4:24, XREAL_1:66;
then p . i <= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A2, A3, B7;
hence p . i <= q . i by A4, A5, B7; :: thesis: verum

end;

then Sum p <= Sum q by RVSUM_1:112;
hence lower_sum f,D <= upper_sum f,D by A2, A6, Def8, A3; :: thesis: verum