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_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))) )
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;
A5: dom f = A by FUNCT_2:def 1;
assume i in dom D ; :: thesis: (lower_bound (rng f)) * (vol (divset (D,i))) <= (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
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_below by A1, Th9;
hence (lower_bound (rng f)) * (vol (divset (D,i))) <= (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A3, A6, A4, SEQ_4:47, XREAL_1:64; :: thesis: verum

end;

A7: 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 A8: 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 A8, Th17; :: thesis: verum

end;

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

proof

len (lower_volume ((chi (A,A)),D)) = len ((lower_bound (rng f)) * (lower_volume ((chi (A,A)),D))) by FINSEQ_2:33;
then A9: len ((lower_bound (rng f)) * (lower_volume ((chi (A,A)),D))) = len D by Def6;
deffunc H₁( Nat) -> Element of REAL = In (((lower_bound (rng (f | (divset (D,$1))))) * (vol (divset (D,$1)))),REAL);
deffunc H₂( set ) -> Element of REAL = In (((lower_bound (rng f)) * ((lower_volume ((chi (A,A)),D)) . $1)),REAL);
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;
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 that
A12: 1 <= i and
A13: i <= len p ; :: thesis: p . i = ((lower_bound (rng f)) * (lower_volume ((chi (A,A)),D))) . i
i in Seg (len D) by A10, A12, A13, FINSEQ_1:1;
then p . i = H₂(i) by A10, A11;
hence p . i = ((lower_bound (rng f)) * (lower_volume ((chi (A,A)),D))) . i by RVSUM_1:44; :: thesis: verum

end;

then A14: p = (lower_bound (rng f)) * (lower_volume ((chi (A,A)),D)) by A10, A9, FINSEQ_1:14;
reconsider p = p as Element of (len D) -tuples_on REAL by A10, FINSEQ_2:92;
consider q being FinSequence of REAL such that
A15: ( len q = len D & ( for i being Nat st i in dom q holds
q . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A16: for i being Nat st i in dom q holds
q . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))

proof

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

end;

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

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

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

end;

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

end;

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