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_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

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_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

let f be Function of A,REAL; :: thesis: for D being Division of A st f | A is bounded_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

let D be Division of A; :: thesis: ( f | A is bounded_above & r <= 0 implies lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) )
assume A1: ( f | A is bounded_above & r <= 0 ) ; :: thesis: lower_sum ((r (#) f),D) = r * (upper_sum (f,D))
A2: for i being Nat st 1 <= i & i <= len (lower_volume ((r (#) f),D)) holds
(lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) implies (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i )
assume A3: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) ) ; :: thesis: (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
len D = len (lower_volume ((r (#) f),D)) by INTEGRA1:def 7;
then i in dom D by ;
then (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) by
.= (r * (upper_volume (f,D))) . i by RVSUM_1:44 ;
hence (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ; :: thesis: verum
end;
len (lower_volume ((r (#) f),D)) = len D by INTEGRA1:def 7
.= len (upper_volume (f,D)) by INTEGRA1:def 6
.= len (r * (upper_volume (f,D))) by NEWTON:2 ;
then lower_volume ((r (#) f),D) = r * (upper_volume (f,D)) by ;
then lower_sum ((r (#) f),D) = Sum (r * (upper_volume (f,D))) by INTEGRA1:def 9
.= r * (Sum (upper_volume (f,D))) by RVSUM_1:87
.= r * (upper_sum (f,D)) by INTEGRA1:def 8 ;
hence lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) ; :: thesis: verum