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;

A11: now

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

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

A13: for D being set st D in divs A holds
(upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

proof

let D be set ; :: thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D )
assume A14: 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, A12, Th27
.= r * ((upper_sum_set f) . D) by INTEGRA1:def 10
.= (r (#) (upper_sum_set f)) . D by A14, RFUNCT_1:57 ;
hence (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

end;

A16: divs A = dom (upper_sum_set f) by FUNCT_2:def 1
.= 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 A16, A13, FUNCT_1:2;
then A17: 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, A12, Th15
.= r * (upper_integral f) by INTEGRA1:def 14 ;
A18: for D being set st D in divs A holds
(lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

proof

let D be set ; :: thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D )
assume A19: 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, A12, Th29
.= r * ((lower_sum_set f) . D) by INTEGRA1:def 11
.= (r (#) (lower_sum_set f)) . D by A19, RFUNCT_1:57 ;
hence (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

end;

A21: divs A = dom (lower_sum_set f) by FUNCT_2:def 1
.= 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 A21, A18, 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, A12, 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 A17; :: thesis: upper_integral (r (#) f) = r * (integral f)
thus upper_integral (r (#) f) = r * (integral f) by A17, INTEGRA1:def 17; :: thesis: verum

end;

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

A23: for D being set st D in divs A holds
(upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D

proof

let D be set ; :: thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D )
assume A24: 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, A22, Th30
.= r * ((lower_sum_set f) . D) by INTEGRA1:def 11
.= (r (#) (lower_sum_set f)) . D by A24, RFUNCT_1:57 ;
hence (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

end;

A26: divs A = dom (lower_sum_set f) by FUNCT_2:def 1
.= 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 A26, A23, FUNCT_1:2;
then A27: 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, A22, Th14
.= r * (lower_integral f) by INTEGRA1:def 15 ;
A28: for D being set st D in divs A holds
(lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D

proof

let D be set ; :: thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D )
assume A29: 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, A22, Th28
.= r * ((upper_sum_set f) . D) by INTEGRA1:def 10
.= (r (#) (upper_sum_set f)) . D by A29, RFUNCT_1:57 ;
hence (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

end;

A31: divs A = dom (upper_sum_set f) by FUNCT_2:def 1
.= 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 A31, A28, 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, A22, 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 A27; :: thesis: upper_integral (r (#) f) = r * (integral f)
upper_integral (r (#) f) = r * (upper_integral f) by A2, A27, INTEGRA1:def 16
.= r * (integral f) by INTEGRA1:def 17 ;
hence upper_integral (r (#) f) = r * (integral f) ; :: thesis: verum

end;

end;

end;

ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D

proof

now

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

suppose A32: r >= 0 ; :: thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D

for D being set 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

proof

let D be set ; :: 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, A32, Th21; :: thesis: verum

end;

hence ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

end;

suppose A33: r < 0 ; :: thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D

for D being set 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

proof

let D be set ; :: 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, A33, Th22; :: thesis: verum

end;

hence ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D ; :: thesis: verum

end;

end;

end;

hence ex a being Real st
for D being set 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;
then rng (lower_sum_set (r (#) f)) is bounded_above by INTEGRA1:13;
then A34: r (#) f is lower_integrable by INTEGRA1:def 13;
ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D

proof

now

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

suppose A35: r >= 0 ; :: thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D

for D being set 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

proof

let D be set ; :: 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, A35, Th19; :: thesis: verum

end;

hence ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

end;

suppose A36: r < 0 ; :: thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D

for D being set 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

proof

let D be set ; :: 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, A36, Th20; :: thesis: verum

end;

hence ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D ; :: thesis: verum

end;

end;

end;

hence ex a being Real st
for D being set 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;
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 A34, A11, INTEGRA1:def 16, INTEGRA1:def 17; :: thesis: verum