let A be non empty closed_interval Subset of REAL; 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; 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; 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; 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; ( 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
; (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 7;
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:11;
then
rng (f | (divset (D,i))) is bounded_below
by RELAT_1:70, XXREAL_2:44;
then
( 0 <= vol (divset (D,i)) & lower_bound (rng (f | (divset (D,i)))) <= r )
by A4, INTEGRA1:9, SEQ_4:def 2;
hence
(lower_volume (f,D)) . i <= F . i
by A5, A3, XREAL_1:64; verum