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) )
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
A1: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_2:sch 1();
assume A2: f | A is bounded ; :: thesis: lower_sum (f,D) <= upper_sum (f,D)
then A3: rng f is bounded_above by Th15;
A4: dom p = dom D by A1, FINSEQ_3:31;
reconsider p = p as Element of (len D) -tuples_on REAL by A1, FINSEQ_2:110;
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
A5: ( len q = len D & ( for i being Nat st i in dom q holds
q . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A6: dom q = dom D by A5, FINSEQ_3:31;
then A7: q = upper_volume (f,D) by A5, Def7;
reconsider q = q as Element of (len D) -tuples_on REAL by A5, FINSEQ_2:110;
A8: rng f is bounded_below by A2, Th13;
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 )
A9: dom f = A by FUNCT_2:def 1;
assume A10: i in Seg (len D) ; :: thesis: p . i <= q . i
then A11: i in dom D by FINSEQ_1:def 3;
i in dom D by A10, FINSEQ_1:def 3;
then dom (f | (divset (D,i))) = divset (D,i) by A9, Th10, RELAT_1:91;
then A12: rng (f | (divset (D,i))) is non empty Subset of REAL by RELAT_1:65;
A13: 0 <= vol (divset (D,i)) by SEQ_4:24, XREAL_1:50;
A14: rng (f | (divset (D,i))) is bounded_above by A3, RELAT_1:99, XXREAL_2:43;
rng (f | (divset (D,i))) is bounded_below by A8, RELAT_1:99, XXREAL_2:44;
then (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) <= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A14, A12, A13, SEQ_4:24, XREAL_1:66;
then p . i <= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A1, A4, A11;
hence p . i <= q . i by A5, A6, A11; :: thesis: verum

end;

then Sum p <= Sum q by RVSUM_1:112;
hence lower_sum (f,D) <= upper_sum (f,D) by A1, A4, A7, Def8; :: thesis: verum