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_below holds
(lower_bound (rng f)) * (vol A) <= lower_sum f,D
let D be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded_below holds
(lower_bound (rng f)) * (vol A) <= lower_sum f,D
let f be Function of A,REAL ; :: thesis: ( f | A is bounded_below implies (lower_bound (rng f)) * (vol A) <= lower_sum f,D )
assume A1: f | A is bounded_below ; :: thesis: (lower_bound (rng f)) * (vol A) <= lower_sum f,D
A2: for i being Element of NAT st i in dom D holds
(lower_bound (rng f)) * (vol (divset D,i)) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i))

proof

let i be Element of NAT ; :: thesis: ( i in dom D implies (lower_bound (rng f)) * (vol (divset D,i)) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) )
assume A3: i in dom D ; :: thesis: (lower_bound (rng f)) * (vol (divset D,i)) <= (lower_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;
dom (f | (divset D,i)) = divset D,i by A6, Th10, A3, 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_below by A1, Th13;
0 <= vol (divset D,i) by SEQ_4:24, XREAL_1:50;
hence (lower_bound (rng f)) * (vol (divset D,i)) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A4, A5, A7, SEQ_4:64, XREAL_1:66; :: thesis: verum

end;

A8: for i being Element of NAT st i in dom D holds
(lower_bound (rng f)) * ((lower_volume (chi A,A),D) . i) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i))

proof

let i be Element of NAT ; :: thesis: ( i in dom D implies (lower_bound (rng f)) * ((lower_volume (chi A,A),D) . i) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) )
assume A9: i in dom D ; :: thesis: (lower_bound (rng f)) * ((lower_volume (chi A,A),D) . i) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i))
then (lower_bound (rng f)) * (vol (divset D,i)) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A2;
hence (lower_bound (rng f)) * ((lower_volume (chi A,A),D) . i) <= (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A9, Th21; :: thesis: verum

end;

Sum ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) <= Sum (lower_volume f,D)

proof

deffunc H₁( set ) -> Element of REAL = (lower_bound (rng f)) * ((lower_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 = (lower_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 = lower_volume f,D by A12, Def8, A13;
len (lower_volume (chi A,A),D) = len ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) by FINSEQ_2:37;
then A15: len ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) = len D by Def8;
for i being Nat st 1 <= i & i <= len p holds
p . i = ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len p implies p . i = ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) . i )
assume ( 1 <= i & i <= len p ) ; :: thesis: p . i = ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) . i
then i in Seg (len D) by A10, FINSEQ_1:3;
then p . i = (lower_bound (rng f)) * ((lower_volume (chi A,A),D) . i) by A10, A11;
hence p . i = ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) . i by RVSUM_1:66; :: thesis: verum

end;

then A16: p = (lower_bound (rng f)) * (lower_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 p . i <= q . i )
assume A17: i in Seg (len D) ; :: thesis: p . i <= q . i
then A18: p . i = (lower_bound (rng f)) * ((lower_volume (chi A,A),D) . i) by A10, A11;
X: i in dom D by A17, FINSEQ_1:def 3;
then q . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A12, A13;
hence p . i <= q . i by A8, A18, X; :: thesis: verum

end;

hence Sum ((lower_bound (rng f)) * (lower_volume (chi A,A),D)) <= Sum (lower_volume f,D) by A14, A16, RVSUM_1:112; :: thesis: verum

end;

then (lower_bound (rng f)) * (Sum (lower_volume (chi A,A),D)) <= Sum (lower_volume f,D) by RVSUM_1:117;
hence (lower_bound (rng f)) * (vol A) <= lower_sum f,D by Th25; :: thesis: verum