let r be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded & f is integrable holds

( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds

( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable implies ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) )

assume that

A1: f | A is bounded and

A2: f is integrable ; :: thesis: ( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

f is upper_integrable by A2, INTEGRA1:def 16;

then A3: rng (upper_sum_set f) is bounded_below by INTEGRA1:def 12;

f is lower_integrable by A2, INTEGRA1:def 16;

then A4: rng (lower_sum_set f) is bounded_above by INTEGRA1:def 13;

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D

then rng (lower_sum_set (r (#) f)) is bounded_above by INTEGRA1:13;

then A24: r (#) f is lower_integrable by INTEGRA1:def 13;

ex a being Real st

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D

then rng (upper_sum_set (r (#) f)) is bounded_below by INTEGRA1:11;

then r (#) f is upper_integrable by INTEGRA1:def 12;

hence ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) by A24, A5, INTEGRA1:def 16, INTEGRA1:def 17; :: thesis: verum

for f being Function of A,REAL st f | A is bounded & f is integrable holds

( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds

( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable implies ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) )

assume that

A1: f | A is bounded and

A2: f is integrable ; :: thesis: ( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

f is upper_integrable by A2, INTEGRA1:def 16;

then A3: rng (upper_sum_set f) is bounded_below by INTEGRA1:def 12;

f is lower_integrable by A2, INTEGRA1:def 16;

then A4: rng (lower_sum_set f) is bounded_above by INTEGRA1:def 13;

A5: now :: thesis: ( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) )end;

ex a being Real st per cases
( r >= 0 or r < 0 )
;

end;

suppose A6:
r >= 0
; :: thesis: ( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) )

A7:
for D being object st D in divs A holds

(upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (upper_sum_set (r (#) f)) by FUNCT_2:def 1;

then upper_sum_set (r (#) f) = r (#) (upper_sum_set f) by A9, A7, FUNCT_1:2;

then A10: upper_integral (r (#) f) = lower_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def 14

.= lower_bound (r ** (rng (upper_sum_set f))) by Th17

.= r * (lower_bound (rng (upper_sum_set f))) by A3, A6, Th15

.= r * (upper_integral f) by INTEGRA1:def 14 ;

A11: for D being object st D in divs A holds

(lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (lower_sum_set (r (#) f)) by FUNCT_2:def 1;

then lower_sum_set (r (#) f) = r (#) (lower_sum_set f) by A13, A11, FUNCT_1:2;

then lower_integral (r (#) f) = upper_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def 15

.= upper_bound (r ** (rng (lower_sum_set f))) by Th17

.= r * (upper_bound (rng (lower_sum_set f))) by A4, A6, Th13

.= r * (lower_integral f) by INTEGRA1:def 15

.= r * (upper_integral f) by A2, INTEGRA1:def 16 ;

hence upper_integral (r (#) f) = lower_integral (r (#) f) by A10; :: thesis: upper_integral (r (#) f) = r * (integral f)

thus upper_integral (r (#) f) = r * (integral f) by A10, INTEGRA1:def 17; :: thesis: verum

end;(upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

proof

A9: divs A =
dom (upper_sum_set f)
by FUNCT_2:def 1
let D be object ; :: thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D )

assume A8: D in divs A ; :: thesis: (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def 10

.= r * (upper_sum (f,D)) by A1, A6, Th27

.= r * ((upper_sum_set f) . D) by INTEGRA1:def 10

.= (r (#) (upper_sum_set f)) . D by A8, RFUNCT_1:57 ;

hence (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

end;assume A8: D in divs A ; :: thesis: (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def 10

.= r * (upper_sum (f,D)) by A1, A6, Th27

.= r * ((upper_sum_set f) . D) by INTEGRA1:def 10

.= (r (#) (upper_sum_set f)) . D by A8, RFUNCT_1:57 ;

hence (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (upper_sum_set (r (#) f)) by FUNCT_2:def 1;

then upper_sum_set (r (#) f) = r (#) (upper_sum_set f) by A9, A7, FUNCT_1:2;

then A10: upper_integral (r (#) f) = lower_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def 14

.= lower_bound (r ** (rng (upper_sum_set f))) by Th17

.= r * (lower_bound (rng (upper_sum_set f))) by A3, A6, Th15

.= r * (upper_integral f) by INTEGRA1:def 14 ;

A11: for D being object st D in divs A holds

(lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

proof

A13: divs A =
dom (lower_sum_set f)
by FUNCT_2:def 1
let D be object ; :: thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D )

assume A12: D in divs A ; :: thesis: (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def 11

.= r * (lower_sum (f,D)) by A1, A6, Th29

.= r * ((lower_sum_set f) . D) by INTEGRA1:def 11

.= (r (#) (lower_sum_set f)) . D by A12, RFUNCT_1:57 ;

hence (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

end;assume A12: D in divs A ; :: thesis: (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def 11

.= r * (lower_sum (f,D)) by A1, A6, Th29

.= r * ((lower_sum_set f) . D) by INTEGRA1:def 11

.= (r (#) (lower_sum_set f)) . D by A12, RFUNCT_1:57 ;

hence (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (lower_sum_set (r (#) f)) by FUNCT_2:def 1;

then lower_sum_set (r (#) f) = r (#) (lower_sum_set f) by A13, A11, FUNCT_1:2;

then lower_integral (r (#) f) = upper_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def 15

.= upper_bound (r ** (rng (lower_sum_set f))) by Th17

.= r * (upper_bound (rng (lower_sum_set f))) by A4, A6, Th13

.= r * (lower_integral f) by INTEGRA1:def 15

.= r * (upper_integral f) by A2, INTEGRA1:def 16 ;

hence upper_integral (r (#) f) = lower_integral (r (#) f) by A10; :: thesis: upper_integral (r (#) f) = r * (integral f)

thus upper_integral (r (#) f) = r * (integral f) by A10, INTEGRA1:def 17; :: thesis: verum

suppose A14:
r < 0
; :: thesis: ( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) )

A15:
for D being object st D in divs A holds

(upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (upper_sum_set (r (#) f)) by FUNCT_2:def 1;

then upper_sum_set (r (#) f) = r (#) (lower_sum_set f) by A17, A15, FUNCT_1:2;

then A18: upper_integral (r (#) f) = lower_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def 14

.= lower_bound (r ** (rng (lower_sum_set f))) by Th17

.= r * (upper_bound (rng (lower_sum_set f))) by A4, A14, Th14

.= r * (lower_integral f) by INTEGRA1:def 15 ;

A19: for D being object st D in divs A holds

(lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (lower_sum_set (r (#) f)) by FUNCT_2:def 1;

then lower_sum_set (r (#) f) = r (#) (upper_sum_set f) by A21, A19, FUNCT_1:2;

then lower_integral (r (#) f) = upper_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def 15

.= upper_bound (r ** (rng (upper_sum_set f))) by Th17

.= r * (lower_bound (rng (upper_sum_set f))) by A3, A14, Th16

.= r * (upper_integral f) by INTEGRA1:def 14

.= r * (lower_integral f) by A2, INTEGRA1:def 16 ;

hence upper_integral (r (#) f) = lower_integral (r (#) f) by A18; :: thesis: upper_integral (r (#) f) = r * (integral f)

upper_integral (r (#) f) = r * (upper_integral f) by A2, A18, INTEGRA1:def 16

.= r * (integral f) by INTEGRA1:def 17 ;

hence upper_integral (r (#) f) = r * (integral f) ; :: thesis: verum

end;(upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

proof

A17: divs A =
dom (lower_sum_set f)
by FUNCT_2:def 1
let D be object ; :: thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D )

assume A16: D in divs A ; :: thesis: (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def 10

.= r * (lower_sum (f,D)) by A1, A14, Th30

.= r * ((lower_sum_set f) . D) by INTEGRA1:def 11

.= (r (#) (lower_sum_set f)) . D by A16, RFUNCT_1:57 ;

hence (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

end;assume A16: D in divs A ; :: thesis: (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def 10

.= r * (lower_sum (f,D)) by A1, A14, Th30

.= r * ((lower_sum_set f) . D) by INTEGRA1:def 11

.= (r (#) (lower_sum_set f)) . D by A16, RFUNCT_1:57 ;

hence (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (upper_sum_set (r (#) f)) by FUNCT_2:def 1;

then upper_sum_set (r (#) f) = r (#) (lower_sum_set f) by A17, A15, FUNCT_1:2;

then A18: upper_integral (r (#) f) = lower_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def 14

.= lower_bound (r ** (rng (lower_sum_set f))) by Th17

.= r * (upper_bound (rng (lower_sum_set f))) by A4, A14, Th14

.= r * (lower_integral f) by INTEGRA1:def 15 ;

A19: for D being object st D in divs A holds

(lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

proof

A21: divs A =
dom (upper_sum_set f)
by FUNCT_2:def 1
let D be object ; :: thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D )

assume A20: D in divs A ; :: thesis: (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def 11

.= r * (upper_sum (f,D)) by A1, A14, Th28

.= r * ((upper_sum_set f) . D) by INTEGRA1:def 10

.= (r (#) (upper_sum_set f)) . D by A20, RFUNCT_1:57 ;

hence (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

end;assume A20: D in divs A ; :: thesis: (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

then reconsider D = D as Division of A by INTEGRA1:def 3;

(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def 11

.= r * (upper_sum (f,D)) by A1, A14, Th28

.= r * ((upper_sum_set f) . D) by INTEGRA1:def 10

.= (r (#) (upper_sum_set f)) . D by A20, RFUNCT_1:57 ;

hence (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;

divs A = dom (lower_sum_set (r (#) f)) by FUNCT_2:def 1;

then lower_sum_set (r (#) f) = r (#) (upper_sum_set f) by A21, A19, FUNCT_1:2;

then lower_integral (r (#) f) = upper_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def 15

.= upper_bound (r ** (rng (upper_sum_set f))) by Th17

.= r * (lower_bound (rng (upper_sum_set f))) by A3, A14, Th16

.= r * (upper_integral f) by INTEGRA1:def 14

.= r * (lower_integral f) by A2, INTEGRA1:def 16 ;

hence upper_integral (r (#) f) = lower_integral (r (#) f) by A18; :: thesis: upper_integral (r (#) f) = r * (integral f)

upper_integral (r (#) f) = r * (upper_integral f) by A2, A18, INTEGRA1:def 16

.= r * (integral f) by INTEGRA1:def 17 ;

hence upper_integral (r (#) f) = r * (integral f) ; :: thesis: verum

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D

proof

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

end;

then
(lower_sum_set (r (#) f)) | (divs A) is bounded_above
by RFUNCT_1:70;now :: thesis: ex a being Real st

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . Dend;

hence
ex a being Real st for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D

per cases
( r >= 0 or r < 0 )
;

end;

suppose A22:
r >= 0
; :: thesis: ex a being Real st

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

(r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

end;(r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

proof

hence
ex a being Real st
let D be object ; :: thesis: ( D in (divs A) /\ (dom (lower_sum_set (r (#) f))) implies (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D )

assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; :: thesis: (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A22, Th21; :: thesis: verum

end;assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; :: thesis: (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A22, Th21; :: thesis: verum

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

suppose A23:
r < 0
; :: thesis: ex a being Real st

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

(r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

end;(r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

proof

hence
ex a being Real st
let D be object ; :: thesis: ( D in (divs A) /\ (dom (lower_sum_set (r (#) f))) implies (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D )

assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; :: thesis: (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A23, Th22; :: thesis: verum

end;assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; :: thesis: (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A23, Th22; :: thesis: verum

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

for D being object st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds

a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

then rng (lower_sum_set (r (#) f)) is bounded_above by INTEGRA1:13;

then A24: r (#) f is lower_integrable by INTEGRA1:def 13;

ex a being Real st

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D

proof

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

end;

then
(upper_sum_set (r (#) f)) | (divs A) is bounded_below
by RFUNCT_1:71;now :: thesis: ex a being Real st

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . Dend;

hence
ex a being Real st for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D

per cases
( r >= 0 or r < 0 )
;

end;

suppose A25:
r >= 0
; :: thesis: ex a being Real st

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

(r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

end;(r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

proof

hence
ex a being Real st
let D be object ; :: thesis: ( D in (divs A) /\ (dom (upper_sum_set (r (#) f))) implies (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D )

assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; :: thesis: (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A25, Th19; :: thesis: verum

end;assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; :: thesis: (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A25, Th19; :: thesis: verum

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

suppose A26:
r < 0
; :: thesis: ex a being Real st

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

(r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

end;(r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

proof

hence
ex a being Real st
let D be object ; :: thesis: ( D in (divs A) /\ (dom (upper_sum_set (r (#) f))) implies (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D )

assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; :: thesis: (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A26, Th20; :: thesis: verum

end;assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; :: thesis: (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

then D is Division of A by INTEGRA1:def 3;

hence (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A26, Th20; :: thesis: verum

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

for D being object st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds

a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

then rng (upper_sum_set (r (#) f)) is bounded_below by INTEGRA1:11;

then r (#) f is upper_integrable by INTEGRA1:def 12;

hence ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) by A24, A5, INTEGRA1:def 16, INTEGRA1:def 17; :: thesis: verum