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_above holds
upper_sum (f,D) <= (upper_bound (rng f)) * (vol A)
let D be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded_above holds
upper_sum (f,D) <= (upper_bound (rng f)) * (vol A)
let f be Function of A,REAL; :: thesis: ( f | A is bounded_above implies upper_sum (f,D) <= (upper_bound (rng f)) * (vol A) )
assume A1: f | A is bounded_above ; :: thesis: upper_sum (f,D) <= (upper_bound (rng f)) * (vol A)
A2: for i being Element of NAT st i in Seg (len D) holds
(upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))

proof

let i be Element of NAT ; :: thesis: ( i in Seg (len D) implies (upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
A3: rng (f | (divset (D,i))) c= rng f by RELAT_1:70;
A4: 0 <= vol (divset (D,i)) by SEQ_4:11, XREAL_1:48;
assume i in Seg (len D) ; :: thesis: (upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
then A5: i in dom D by FINSEQ_1:def 3;
dom f = A by FUNCT_2:def 1;
then dom (f | (divset (D,i))) = divset (D,i) by A5, Th6, RELAT_1:62;
then A6: rng (f | (divset (D,i))) is non empty Subset of REAL by RELAT_1:42;
rng f is bounded_above by A1, Th11;
hence (upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A3, A6, A4, SEQ_4:48, XREAL_1:64; :: thesis: verum

end;

A7: for i being Element of NAT st i in Seg (len D) holds
(upper_bound (rng f)) * ((upper_volume ((chi (A,A)),D)) . i) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))

proof

let i be Element of NAT ; :: thesis: ( i in Seg (len D) implies (upper_bound (rng f)) * ((upper_volume ((chi (A,A)),D)) . i) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
assume A8: i in Seg (len D) ; :: thesis: (upper_bound (rng f)) * ((upper_volume ((chi (A,A)),D)) . i) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
then A9: i in dom D by FINSEQ_1:def 3;
(upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A2, A8;
hence (upper_bound (rng f)) * ((upper_volume ((chi (A,A)),D)) . i) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A9, Th18; :: thesis: verum

end;

Sum ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) >= Sum (upper_volume (f,D))

proof

len (upper_volume ((chi (A,A)),D)) = len ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) by FINSEQ_2:33;
then A10: len ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) = len D by Def5;
deffunc H₁( Nat) -> Element of REAL = In (((upper_bound (rng (f | (divset (D,$1))))) * (vol (divset (D,$1)))),REAL);
deffunc H₂( set ) -> Element of REAL = In (((upper_bound (rng f)) * ((upper_volume ((chi (A,A)),D)) . $1)),REAL);
consider p being FinSequence of REAL such that
A11: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A12: dom p = Seg (len D) by A11, FINSEQ_1:def 3;
for i being Nat st 1 <= i & i <= len p holds
p . i = ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len p implies p . i = ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) . i )
assume that
A13: 1 <= i and
A14: i <= len p ; :: thesis: p . i = ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) . i
i in Seg (len D) by A11, A13, A14, FINSEQ_1:1;
then p . i = H₂(i) by A11, A12;
hence p . i = ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) . i by RVSUM_1:44; :: thesis: verum

end;

then A15: p = (upper_bound (rng f)) * (upper_volume ((chi (A,A)),D)) by A11, A10, FINSEQ_1:14;
reconsider p = p as Element of (len D) -tuples_on REAL by A11, FINSEQ_2:92;
consider q being FinSequence of REAL such that
A16: ( len q = len D & ( for i being Nat st i in dom q holds
q . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A17: 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 A16;
hence q . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ; :: thesis: verum

end;

A18: dom q = dom D by A16, FINSEQ_3:29;
then A19: q = upper_volume (f,D) by A16, Def5, A17;
reconsider q = q as Element of (len D) -tuples_on REAL by A16, FINSEQ_2:92;

now :: thesis: for i being Nat st i in Seg (len D) holds
q . i <= p . i

let i be Nat; :: thesis: ( i in Seg (len D) implies q . i <= p . i )
assume A20: i in Seg (len D) ; :: thesis: q . i <= p . i
then i in dom D by FINSEQ_1:def 3;
then A21: q . i = H₁(i) by A16, A18;
p . i = H₂(i) by A11, A12, A20;
hence q . i <= p . i by A7, A20, A21; :: thesis: verum

end;

hence Sum ((upper_bound (rng f)) * (upper_volume ((chi (A,A)),D))) >= Sum (upper_volume (f,D)) by A19, A15, RVSUM_1:82; :: thesis: verum

end;

then (upper_bound (rng f)) * (Sum (upper_volume ((chi (A,A)),D))) >= Sum (upper_volume (f,D)) by RVSUM_1:87;
hence upper_sum (f,D) <= (upper_bound (rng f)) * (vol A) by Th22; :: thesis: verum