let A be non empty 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 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; :: thesis: verum

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 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; :: thesis: verum