let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume f,D) . i <= F . i
let f be Function of A,REAL ; :: thesis: for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume f,D) . i <= F . i
let D be Division of A; :: thesis: for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume f,D) . i <= F . i
let F be middle_volume of f,D; :: thesis: for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume f,D) . i <= F . i
let i be Nat; :: thesis: ( f | A is bounded_below & i in dom D implies (lower_volume f,D) . i <= F . i )
assume that
A1: f | A is bounded_below and
A2: i in dom D ; :: thesis: (lower_volume f,D) . i <= F . i
A3: (lower_volume f,D) . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A2, INTEGRA1:def 8;
consider r being Element of REAL such that
A4: r in rng (f | (divset D,i)) and
A5: F . i = r * (vol (divset D,i)) by A2, Def1;
rng f is bounded_below by A1, INTEGRA1:13;
then rng (f | (divset D,i)) is bounded_below by RELAT_1:99, XXREAL_2:44;
then ( 0 <= vol (divset D,i) & lower_bound (rng (f | (divset D,i))) <= r ) by A4, INTEGRA1:11, SEQ_4:def 5;
hence (lower_volume f,D) . i <= F . i by A5, A3, XREAL_1:66; :: thesis: verum