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_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 AS: ( f | A is bounded_above & i in dom D ) ; :: thesis: F . i <= (upper_volume f,D) . i
consider r being Element of REAL such that
P1: ( r in rng (f | (divset D,i)) & F . i = r * (vol (divset D,i)) ) by defx0, AS;
P2: (upper_volume f,D) . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by INTEGRA1:def 7, AS;
P3: 0 <= vol (divset D,i) by INTEGRA1:11;
( rng (f | (divset D,i)) is bounded_above & not rng (f | (divset D,i)) is empty )

proof

rng f is bounded_above by AS, INTEGRA1:15;
hence rng (f | (divset D,i)) is bounded_above by RELAT_1:99, XXREAL_2:43; :: thesis: not rng (f | (divset D,i)) is empty
dom f = A by FUNCT_2:def 1;
then dom (f | (divset D,i)) = divset D,i by INTEGRA1:10, AS, RELAT_1:91;
hence not rng (f | (divset D,i)) is empty by RELAT_1:65; :: thesis: verum

end;

then r <= upper_bound (rng (f | (divset D,i))) by SEQ_4:def 4, P1;
hence F . i <= (upper_volume f,D) . i by P1, P2, P3, XREAL_1:66; :: thesis: verum