let r be Real; :: thesis: for A being 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 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 7;
then i in dom D by A3, FINSEQ_3:27;
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:66 ;
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 7
.= len (lower_volume f,D) by INTEGRA1:def 8
.= len (r * (lower_volume f,D)) by NEWTON:6 ;
then upper_volume (r (#) f),D = r * (lower_volume f,D) by A2, FINSEQ_1:18;
then upper_sum (r (#) f),D = Sum (r * (lower_volume f,D)) by INTEGRA1:def 9
.= r * (Sum (lower_volume f,D)) by RVSUM_1:117
.= r * (lower_sum f,D) by INTEGRA1:def 10 ;
hence upper_sum (r (#) f),D = r * (lower_sum f,D) ; :: thesis: verum