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
upper_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
upper_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
upper_sum ((r (#) f),D) = r * (upper_sum (f,D))

let D be Division of A; :: thesis: ( f | A is bounded_above & r >= 0 implies upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) )
assume A1: ( f | A is bounded_above & r >= 0 ) ; :: thesis: upper_sum ((r (#) f),D) = r * (upper_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 * (upper_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 * (upper_volume (f,D))) . i )
assume A3: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) ) ; :: thesis: (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
len D = len (upper_volume ((r (#) f),D)) by INTEGRA1:def 6;
then i in dom D by ;
then (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) by
.= (r * (upper_volume (f,D))) . i by RVSUM_1:44 ;
hence (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ; :: thesis: verum
end;
len (upper_volume ((r (#) f),D)) = len D by INTEGRA1:def 6
.= len (upper_volume (f,D)) by INTEGRA1:def 6
.= len (r * (upper_volume (f,D))) by NEWTON:2 ;
then upper_volume ((r (#) f),D) = r * (upper_volume (f,D)) by ;
then upper_sum ((r (#) f),D) = Sum (r * (upper_volume (f,D))) by INTEGRA1:def 8
.= r * (Sum (upper_volume (f,D))) by RVSUM_1:87
.= r * (upper_sum (f,D)) by INTEGRA1:def 8 ;
hence upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) ; :: thesis: verum