let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let f be Function of A,REAL; :: thesis: for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let S be middle_volume_Sequence of f,T; :: thesis: for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let i be Element of NAT ; :: thesis: ( f | A is bounded_above implies (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i )

assume A1: f | A is bounded_above ; :: thesis: (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

( (middle_sum (f,S)) . i = middle_sum (f,(S . i)) & (upper_sum (f,T)) . i = upper_sum (f,(T . i)) ) by Def4, INTEGRA2:def 2;

hence (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i by A1, Th2; :: thesis: verum

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let f be Function of A,REAL; :: thesis: for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let S be middle_volume_Sequence of f,T; :: thesis: for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

let i be Element of NAT ; :: thesis: ( f | A is bounded_above implies (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i )

assume A1: f | A is bounded_above ; :: thesis: (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

( (middle_sum (f,S)) . i = middle_sum (f,(S . i)) & (upper_sum (f,T)) . i = upper_sum (f,(T . i)) ) by Def4, INTEGRA2:def 2;

hence (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i by A1, Th2; :: thesis: verum