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_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:99;
A4: 0 <= vol (divset D,i) by SEQ_4:24, XREAL_1:50;
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, Th10, RELAT_1:91;
then A6: rng (f | (divset D,i)) is non empty Subset of REAL by RELAT_1:65;
rng f is bounded_above by A1, Th15;
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:65, XREAL_1:66; :: 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, Th22; :: 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:37;
then A10: len ((upper_bound (rng f)) * (upper_volume (chi A,A),D)) = len D by Def7;
deffunc H₁( Nat) -> Element of REAL = (upper_bound (rng (f | (divset D,$1)))) * (vol (divset D,$1));
deffunc H₂( set ) -> Element of REAL = (upper_bound (rng f)) * ((upper_volume (chi A,A),D) . $1);
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:3;
then p . i = (upper_bound (rng f)) * ((upper_volume (chi A,A),D) . i) by A11, A12;
hence p . i = ((upper_bound (rng f)) * (upper_volume (chi A,A),D)) . i by RVSUM_1:66; :: thesis: verum

end;

then A15: p = (upper_bound (rng f)) * (upper_volume (chi A,A),D) by A11, A10, FINSEQ_1:18;
reconsider p = p as Element of (len D) -tuples_on REAL by A11, FINSEQ_2:110;
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: dom q = dom D by A16, FINSEQ_3:31;
then A18: q = upper_volume f,D by A16, Def7;
reconsider q = q as Element of (len D) -tuples_on REAL by A16, FINSEQ_2:110;

now

let i be Nat; :: thesis: ( i in Seg (len D) implies q . i <= p . i )
assume A19: i in Seg (len D) ; :: thesis: q . i <= p . i
then i in dom D by FINSEQ_1:def 3;
then A20: q . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A16, A17;
p . i = (upper_bound (rng f)) * ((upper_volume (chi A,A),D) . i) by A11, A12, A19;
hence q . i <= p . i by A7, A19, A20; :: thesis: verum

end;

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

end;

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