let A be non empty 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 = In (((lower_bound (rng (f | (divset (D,$1))))) * (vol (divset (D,$1)))),REAL);
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();
A2: for i being Nat st i in dom p holds
p . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))

proof

let i be Nat; :: thesis: ( i in dom p implies p . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
assume i in dom p ; :: thesis: p . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
then p . i = H₁(i) by A1;
hence p . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ; :: thesis: verum

end;

assume A3: f | A is bounded ; :: thesis: lower_sum (f,D) <= upper_sum (f,D)
then A4: rng f is bounded_above by Th11;
A5: dom p = dom D by A1, FINSEQ_3:29;
reconsider p = p as Element of (len D) -tuples_on REAL by A1, FINSEQ_2:92;
deffunc H₂( Nat) -> Element of REAL = In (((upper_bound (rng (f | (divset (D,$1))))) * (vol (divset (D,$1)))),REAL);
consider q being FinSequence of REAL such that
A6: ( len q = len D & ( for i being Nat st i in dom q holds
q . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A7: for i being Nat st i in dom q holds
q . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))

proof

let i be Nat; :: thesis: ( i in dom q implies q . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
assume i in dom q ; :: thesis: q . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
then q . i = H₂(i) by A6;
hence q . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ; :: thesis: verum

end;

A8: dom q = dom D by A6, FINSEQ_3:29;
then len q = len D by FINSEQ_3:29;
then A9: q = upper_volume (f,D) by A7, Def5, A8;
reconsider q = q as Element of (len D) -tuples_on REAL by A6, FINSEQ_2:92;
A10: rng f is bounded_below by A3, Th9;
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 )
A11: dom f = A by FUNCT_2:def 1;
assume A12: i in Seg (len D) ; :: thesis: p . i <= q . i
then A13: i in dom D by FINSEQ_1:def 3;
i in dom D by A12, FINSEQ_1:def 3;
then dom (f | (divset (D,i))) = divset (D,i) by A11, Th6, RELAT_1:62;
then A14: rng (f | (divset (D,i))) is non empty Subset of REAL by RELAT_1:42;
A15: 0 <= vol (divset (D,i)) by SEQ_4:11, XREAL_1:48;
A16: rng (f | (divset (D,i))) is bounded_above by A4, RELAT_1:70, XXREAL_2:43;
rng (f | (divset (D,i))) is bounded_below by A10, RELAT_1:70, 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 A16, A14, A15, SEQ_4:11, XREAL_1:64;
then p . i <= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A5, A13, A2;
hence p . i <= q . i by A8, A13, A7; :: thesis: verum

end;

then Sum p <= Sum q by RVSUM_1:82;
hence lower_sum (f,D) <= upper_sum (f,D) by A1, A5, A9, Def6, A2; :: thesis: verum