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_above & r >= 0 holds
upper_sum ((r (#) f),D) = r * (upper_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_above & r >= 0 holds
upper_sum ((r (#) f),D) = r * (upper_sum (f,D))
let f be 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 D be Division of A; ( 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 )
; 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;
( 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)) )
;
(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 A3, FINSEQ_3:25;
then (upper_volume ((r (#) f),D)) . i =
r * ((upper_volume (f,D)) . i)
by A1, Th23
.=
(r * (upper_volume (f,D))) . i
by RVSUM_1:44
;
hence
(upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
;
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 A2, FINSEQ_1:14;
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))
; verum