let r be Real; 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
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
let A be 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
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
let f be 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 D be Division of A; ( 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 )
; 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;
( 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)) )
;
(lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i
len D = len (lower_volume ((r (#) f),D))
by INTEGRA1:def 7;
then
i in dom D
by A3, FINSEQ_3:25;
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:44
;
hence
(lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i
;
verum
end;
len (lower_volume ((r (#) f),D)) =
len D
by INTEGRA1:def 7
.=
len (lower_volume (f,D))
by INTEGRA1:def 7
.=
len (r * (lower_volume (f,D)))
by NEWTON:2
;
then
lower_volume ((r (#) f),D) = r * (lower_volume (f,D))
by A2, FINSEQ_1:14;
then lower_sum ((r (#) f),D) =
Sum (r * (lower_volume (f,D)))
by INTEGRA1:def 9
.=
r * (Sum (lower_volume (f,D)))
by RVSUM_1:87
.=
r * (lower_sum (f,D))
by INTEGRA1:def 9
;
hence
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
; verum