let r be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

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

for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

let f be Function of A,REAL; :: thesis: for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

let D be Division of A; :: thesis: ( f | A is bounded & r >= 0 implies (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) )

assume that

A1: f | A is bounded and

A2: r >= 0 ; :: thesis: (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

A3: rng f is bounded_below by A1, INTEGRA1:11;

A4: (r (#) f) | A is bounded by A1, RFUNCT_1:80;

then A5: lower_sum ((r (#) f),D) >= (lower_bound (rng (r (#) f))) * (vol A) by INTEGRA1:25;

(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def 10;

then A6: (upper_sum_set (r (#) f)) . D >= lower_sum ((r (#) f),D) by A4, INTEGRA1:28;

lower_bound (rng (r (#) f)) = lower_bound (r ** (rng f)) by Th17

.= r * (lower_bound (rng f)) by A2, A3, Th15 ;

hence (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; :: thesis: verum

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

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

for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

let f be Function of A,REAL; :: thesis: for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

let D be Division of A; :: thesis: ( f | A is bounded & r >= 0 implies (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) )

assume that

A1: f | A is bounded and

A2: r >= 0 ; :: thesis: (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

A3: rng f is bounded_below by A1, INTEGRA1:11;

A4: (r (#) f) | A is bounded by A1, RFUNCT_1:80;

then A5: lower_sum ((r (#) f),D) >= (lower_bound (rng (r (#) f))) * (vol A) by INTEGRA1:25;

(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def 10;

then A6: (upper_sum_set (r (#) f)) . D >= lower_sum ((r (#) f),D) by A4, INTEGRA1:28;

lower_bound (rng (r (#) f)) = lower_bound (r ** (rng f)) by Th17

.= r * (lower_bound (rng f)) by A2, A3, Th15 ;

hence (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; :: thesis: verum