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)) )
assume A3: 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))
A4: rng (f | (divset D,i)) c= rng f by RELAT_1:99;
A5: rng (f | (divset D,i)) is non empty Subset of REAL

proof

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

end;

A7: rng f is bounded_above by A1, Th15;
0 <= vol (divset D,i) by SEQ_4:24, XREAL_1:50;
hence (upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A4, A5, A7, SEQ_4:65, XREAL_1:66; :: thesis: verum

end;

A8: 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 A9: 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 X: (upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A2;
i in dom D by A9, FINSEQ_1:def 3;
hence (upper_bound (rng f)) * ((upper_volume (chi A,A),D) . i) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by Th22, X; :: thesis: verum

end;

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

proof

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
A10: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A11: dom p = Seg (len D) by A10, FINSEQ_1:def 3;
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
A12: ( len q = len D & ( for i being Nat st i in dom q holds
q . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A13: dom q = dom D by A12, FINSEQ_3:31;
A14: q = upper_volume f,D by A12, Def7, A13;
len (upper_volume (chi A,A),D) = len ((upper_bound (rng f)) * (upper_volume (chi A,A),D)) by FINSEQ_2:37;
then A15: len ((upper_bound (rng f)) * (upper_volume (chi A,A),D)) = len D by Def7;
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 ( 1 <= i & i <= len p ) ; :: thesis: p . i = ((upper_bound (rng f)) * (upper_volume (chi A,A),D)) . i
then i in Seg (len D) by A10, FINSEQ_1:3;
then p . i = (upper_bound (rng f)) * ((upper_volume (chi A,A),D) . i) by A10, A11;
hence p . i = ((upper_bound (rng f)) * (upper_volume (chi A,A),D)) . i by RVSUM_1:66; :: thesis: verum

end;

then A16: p = (upper_bound (rng f)) * (upper_volume (chi A,A),D) by A10, A15, FINSEQ_1:18;
reconsider p = p as Element of (len D) -tuples_on REAL by A10, FINSEQ_2:110;
reconsider q = q as Element of (len D) -tuples_on REAL by A12, FINSEQ_2:110;

now

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

end;

hence Sum ((upper_bound (rng f)) * (upper_volume (chi A,A),D)) >= Sum (upper_volume f,D) by A14, A16, 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