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

lower_sum ((r (#) f),D) = r * (upper_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_above & r <= 0 holds

lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

let f be Function of A,REAL; :: thesis: for D being Division of A st f | A is bounded_above & r <= 0 holds

lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

let D be Division of A; :: thesis: ( f | A is bounded_above & r <= 0 implies lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) )

assume A1: ( f | A is bounded_above & r <= 0 ) ; :: thesis: lower_sum ((r (#) f),D) = r * (upper_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 * (upper_volume (f,D))) . i

.= len (upper_volume (f,D)) by INTEGRA1:def 6

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

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

then lower_sum ((r (#) f),D) = Sum (r * (upper_volume (f,D))) by INTEGRA1:def 9

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

.= r * (upper_sum (f,D)) by INTEGRA1:def 8 ;

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

for f being Function of A,REAL

for D being Division of A st f | A is bounded_above & r <= 0 holds

lower_sum ((r (#) f),D) = r * (upper_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_above & r <= 0 holds

lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

let f be Function of A,REAL; :: thesis: for D being Division of A st f | A is bounded_above & r <= 0 holds

lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

let D be Division of A; :: thesis: ( f | A is bounded_above & r <= 0 implies lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) )

assume A1: ( f | A is bounded_above & r <= 0 ) ; :: thesis: lower_sum ((r (#) f),D) = r * (upper_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 * (upper_volume (f,D))) . i

proof

len (lower_volume ((r (#) f),D)) =
len D
by INTEGRA1:def 7
let i be Nat; :: thesis: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) implies (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i )

assume A3: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) ) ; :: thesis: (lower_volume ((r (#) f),D)) . i = (r * (upper_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 * ((upper_volume (f,D)) . i) by A1, Th24

.= (r * (upper_volume (f,D))) . i by RVSUM_1:44 ;

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

end;assume A3: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) ) ; :: thesis: (lower_volume ((r (#) f),D)) . i = (r * (upper_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 * ((upper_volume (f,D)) . i) by A1, Th24

.= (r * (upper_volume (f,D))) . i by RVSUM_1:44 ;

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

.= len (upper_volume (f,D)) by INTEGRA1:def 6

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

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

then lower_sum ((r (#) f),D) = Sum (r * (upper_volume (f,D))) by INTEGRA1:def 9

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

.= r * (upper_sum (f,D)) by INTEGRA1:def 8 ;

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