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_below & r <= 0 holds

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

.= len (lower_volume (f,D)) by INTEGRA1:def 7

.= len (r * (lower_volume (f,D))) by NEWTON:2 ;

then upper_volume ((r (#) f),D) = r * (lower_volume (f,D)) by A2, FINSEQ_1:14;

then upper_sum ((r (#) f),D) = Sum (r * (lower_volume (f,D))) by INTEGRA1:def 8

.= r * (Sum (lower_volume (f,D))) by RVSUM_1:87

.= r * (lower_sum (f,D)) by INTEGRA1:def 9 ;

hence upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) ; :: thesis: verum

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 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_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

len (upper_volume ((r (#) f),D)) =
len D
by INTEGRA1:def 6
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 6;

then i in dom D by A3, FINSEQ_3:25;

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:44 ;

hence (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ; :: thesis: verum

end;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 6;

then i in dom D by A3, FINSEQ_3:25;

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:44 ;

hence (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ; :: thesis: verum

.= len (lower_volume (f,D)) by INTEGRA1:def 7

.= len (r * (lower_volume (f,D))) by NEWTON:2 ;

then upper_volume ((r (#) f),D) = r * (lower_volume (f,D)) by A2, FINSEQ_1:14;

then upper_sum ((r (#) f),D) = Sum (r * (lower_volume (f,D))) by INTEGRA1:def 8

.= r * (Sum (lower_volume (f,D))) by RVSUM_1:87

.= r * (lower_sum (f,D)) by INTEGRA1:def 9 ;

hence upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) ; :: thesis: verum