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_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_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_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
let f be Function of A,REAL; :: thesis: for D being Division of A st f | A is bounded_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
let D be Division of A; :: thesis: ( f | A is bounded_below & r <= 0 implies upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) )
assume A1: ( f | A is bounded_below & r <= 0 ) ; :: thesis: upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
A2: for i being Nat st 1 <= i & i <= len (upper_volume ((r (#) f),D)) holds
(upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) implies (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i )
assume A3: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) ) ; :: thesis: (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i
len D = len (upper_volume ((r (#) f),D)) by INTEGRA1:def 6;
then i in dom D by A3, FINSEQ_3:25;
then (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) by A1, Th26
.= (r * (lower_volume (f,D))) . i by RVSUM_1:44 ;
hence (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ; :: thesis: verum

end;

len (upper_volume ((r (#) f),D)) = len D by INTEGRA1:def 6
.= len (lower_volume (f,D)) by INTEGRA1:def 7
.= len (r * (lower_volume (f,D))) by NEWTON:2 ;
then upper_volume ((r (#) f),D) = r * (lower_volume (f,D)) by A2, FINSEQ_1:14;
then upper_sum ((r (#) f),D) = Sum (r * (lower_volume (f,D))) by INTEGRA1:def 8
.= r * (Sum (lower_volume (f,D))) by RVSUM_1:87
.= r * (lower_sum (f,D)) by INTEGRA1:def 9 ;
hence upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) ; :: thesis: verum