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
lower_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
lower_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
lower_sum (r (#) f),D = r * (lower_sum f,D)
let D be Division of A; :: thesis: ( f | A is bounded_below & r >= 0 implies lower_sum (r (#) f),D = r * (lower_sum f,D) )
assume A1: ( f | A is bounded_below & r >= 0 ) ; :: thesis: lower_sum (r (#) f),D = r * (lower_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 * (lower_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 * (lower_volume f,D)) . i )
assume A3: ( 1 <= i & i <= len (lower_volume (r (#) f),D) ) ; :: thesis: (lower_volume (r (#) f),D) . i = (r * (lower_volume f,D)) . i
len D = len (lower_volume (r (#) f),D) by INTEGRA1:def 8;
then i in dom D by A3, FINSEQ_3:27;
then (lower_volume (r (#) f),D) . i = r * ((lower_volume f,D) . i) by A1, Th25
.= (r * (lower_volume f,D)) . i by RVSUM_1:66 ;
hence (lower_volume (r (#) f),D) . i = (r * (lower_volume f,D)) . i ; :: thesis: verum

end;

len (lower_volume (r (#) f),D) = len D by INTEGRA1:def 8
.= len (lower_volume f,D) by INTEGRA1:def 8
.= len (r * (lower_volume f,D)) by NEWTON:6 ;
then lower_volume (r (#) f),D = r * (lower_volume f,D) by A2, FINSEQ_1:18;
then lower_sum (r (#) f),D = Sum (r * (lower_volume f,D)) by INTEGRA1:def 10
.= r * (Sum (lower_volume f,D)) by RVSUM_1:117
.= r * (lower_sum f,D) by INTEGRA1:def 10 ;
hence lower_sum (r (#) f),D = r * (lower_sum f,D) ; :: thesis: verum