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_above & i in dom D holds
F . i <= (upper_volume (f,D)) . 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_above & i in dom D holds
F . i <= (upper_volume (f,D)) . 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_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i

let F be middle_volume of f,D; :: thesis: for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i

let i be Nat; :: thesis: ( f | A is bounded_above & i in dom D implies F . i <= (upper_volume (f,D)) . i )
assume that
A1: f | A is bounded_above and
A2: i in dom D ; :: thesis: F . i <= (upper_volume (f,D)) . i
A3: (upper_volume (f,D)) . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by ;
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 ;
rng f is bounded_above by ;
then rng (f | (divset (D,i))) is bounded_above by ;
then ( 0 <= vol (divset (D,i)) & r <= upper_bound (rng (f | (divset (D,i)))) ) by ;
hence F . i <= (upper_volume (f,D)) . i by ; :: thesis: verum