let r be Real; :: thesis: for A being 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 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) )
A3: r (#) f is upper_integrable

proof

rng (upper_sum_set (r (#) f)) is bounded_below

proof

(upper_sum_set (r (#) f)) | (divs A) is bounded_below

proof

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 a1: 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, A1, 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 a1: 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, A1, 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;

hence (upper_sum_set (r (#) f)) | (divs A) is bounded_below by RFUNCT_1:88; :: thesis: verum

end;

hence rng (upper_sum_set (r (#) f)) is bounded_below by INTEGRA1:13; :: thesis: verum

end;

hence r (#) f is upper_integrable by INTEGRA1:def 13; :: thesis: verum

end;

A4: r (#) f is lower_integrable

proof

rng (lower_sum_set (r (#) f)) is bounded_above

proof

(lower_sum_set (r (#) f)) | (divs A) is bounded_above

proof

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 a1: 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, A1, 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 a1: 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, A1, 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;

hence (lower_sum_set (r (#) f)) | (divs A) is bounded_above by RFUNCT_1:87; :: thesis: verum

end;

hence rng (lower_sum_set (r (#) f)) is bounded_above by INTEGRA1:15; :: thesis: verum

end;

hence r (#) f is lower_integrable by INTEGRA1:def 14; :: thesis: verum

end;

( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) )

proof

A5: dom (upper_sum_set f) = divs A by INTEGRA1:def 11;
then A6: upper_sum_set f is total by PARTFUN1:def 4;
then A7: upper_sum_set f is Function of (divs A),REAL ;
A8: not rng (upper_sum_set f) is empty by A5, RELAT_1:65;
( f is upper_integrable & f is lower_integrable ) by A2, INTEGRA1:def 17;
then A9: ( rng (upper_sum_set f) is bounded_below & rng (lower_sum_set f) is bounded_above ) by INTEGRA1:def 13, INTEGRA1:def 14;
A10: dom (lower_sum_set f) = divs A by INTEGRA1:def 12;
then A11: lower_sum_set f is total by PARTFUN1:def 4;
then A12: lower_sum_set f is Function of (divs A),REAL ;
A13: not rng (lower_sum_set f) is empty by A10, RELAT_1:65;
A14: ( f | A is bounded_above & f | A is bounded_below ) by A1;

now

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

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

A16: upper_sum_set (r (#) f) = r (#) (upper_sum_set f)

proof

A17: divs A = dom (upper_sum_set (r (#) f)) by INTEGRA1:def 11;
A18: divs A = dom (upper_sum_set f) by INTEGRA1:def 11
.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;
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 A19: 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;
A20: D in dom (upper_sum_set (r (#) f)) by A19, INTEGRA1:def 11;
A21: D in dom (upper_sum_set f) by A19, INTEGRA1:def 11;
(upper_sum_set (r (#) f)) . D = upper_sum (r (#) f),D by A20, INTEGRA1:def 11
.= r * (upper_sum f,D) by A14, A15, Th27
.= r * ((upper_sum_set f) . D) by A21, INTEGRA1:def 11
.= (r (#) (upper_sum_set f)) . D by A6, A19, RFUNCT_1:73 ;
hence (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

end;

hence upper_sum_set (r (#) f) = r (#) (upper_sum_set f) by A17, A18, FUNCT_1:9; :: thesis: verum

end;

A22: lower_sum_set (r (#) f) = r (#) (lower_sum_set f)

proof

A23: divs A = dom (lower_sum_set (r (#) f)) by INTEGRA1:def 12;
A24: divs A = dom (lower_sum_set f) by INTEGRA1:def 12
.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;
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 A25: 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;
A26: D in dom (lower_sum_set (r (#) f)) by A25, INTEGRA1:def 12;
A27: D in dom (lower_sum_set f) by A25, INTEGRA1:def 12;
(lower_sum_set (r (#) f)) . D = lower_sum (r (#) f),D by A26, INTEGRA1:def 12
.= r * (lower_sum f,D) by A14, A15, Th29
.= r * ((lower_sum_set f) . D) by A27, INTEGRA1:def 12
.= (r (#) (lower_sum_set f)) . D by A11, A25, RFUNCT_1:73 ;
hence (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

end;

hence lower_sum_set (r (#) f) = r (#) (lower_sum_set f) by A23, A24, FUNCT_1:9; :: thesis: verum

end;

A28: upper_integral (r (#) f) = lower_bound (rng (r (#) (upper_sum_set f))) by A16, INTEGRA1:def 15
.= lower_bound (r ** (rng (upper_sum_set f))) by A7, Th17
.= r * (lower_bound (rng (upper_sum_set f))) by A8, A9, A15, Th15
.= r * (upper_integral f) by INTEGRA1:def 15 ;
lower_integral (r (#) f) = upper_bound (rng (r (#) (lower_sum_set f))) by A22, INTEGRA1:def 16
.= upper_bound (r ** (rng (lower_sum_set f))) by A12, Th17
.= r * (upper_bound (rng (lower_sum_set f))) by A9, A13, A15, Th13
.= r * (lower_integral f) by INTEGRA1:def 16
.= r * (upper_integral f) by A2, INTEGRA1:def 17 ;
hence upper_integral (r (#) f) = lower_integral (r (#) f) by A28; :: thesis: upper_integral (r (#) f) = r * (integral f)
thus upper_integral (r (#) f) = r * (integral f) by A28, INTEGRA1:def 18; :: thesis: verum

end;

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

A30: upper_sum_set (r (#) f) = r (#) (lower_sum_set f)

proof

A31: divs A = dom (upper_sum_set (r (#) f)) by INTEGRA1:def 11;
A32: divs A = dom (lower_sum_set f) by INTEGRA1:def 12
.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;
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 A33: 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;
A34: D in dom (upper_sum_set (r (#) f)) by A33, INTEGRA1:def 11;
A35: D in dom (lower_sum_set f) by A33, INTEGRA1:def 12;
(upper_sum_set (r (#) f)) . D = upper_sum (r (#) f),D by A34, INTEGRA1:def 11
.= r * (lower_sum f,D) by A14, A29, Th30
.= r * ((lower_sum_set f) . D) by A35, INTEGRA1:def 12
.= (r (#) (lower_sum_set f)) . D by A11, A33, RFUNCT_1:73 ;
hence (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; :: thesis: verum

end;

hence upper_sum_set (r (#) f) = r (#) (lower_sum_set f) by A31, A32, FUNCT_1:9; :: thesis: verum

end;

A36: lower_sum_set (r (#) f) = r (#) (upper_sum_set f)

proof

A37: divs A = dom (lower_sum_set (r (#) f)) by INTEGRA1:def 12;
A38: divs A = dom (upper_sum_set f) by INTEGRA1:def 11
.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;
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 A39: 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;
A40: D in dom (lower_sum_set (r (#) f)) by A39, INTEGRA1:def 12;
A41: D in dom (upper_sum_set f) by A39, INTEGRA1:def 11;
(lower_sum_set (r (#) f)) . D = lower_sum (r (#) f),D by A40, INTEGRA1:def 12
.= r * (upper_sum f,D) by A14, A29, Th28
.= r * ((upper_sum_set f) . D) by A41, INTEGRA1:def 11
.= (r (#) (upper_sum_set f)) . D by A6, A39, RFUNCT_1:73 ;
hence (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; :: thesis: verum

end;

hence lower_sum_set (r (#) f) = r (#) (upper_sum_set f) by A37, A38, FUNCT_1:9; :: thesis: verum

end;

A42: upper_integral (r (#) f) = lower_bound (rng (r (#) (lower_sum_set f))) by A30, INTEGRA1:def 15
.= lower_bound (r ** (rng (lower_sum_set f))) by A12, Th17
.= r * (upper_bound (rng (lower_sum_set f))) by A9, A13, A29, Th14
.= r * (lower_integral f) by INTEGRA1:def 16 ;
lower_integral (r (#) f) = upper_bound (rng (r (#) (upper_sum_set f))) by A36, INTEGRA1:def 16
.= upper_bound (r ** (rng (upper_sum_set f))) by A7, Th17
.= r * (lower_bound (rng (upper_sum_set f))) by A8, A9, A29, Th16
.= r * (upper_integral f) by INTEGRA1:def 15
.= r * (lower_integral f) by A2, INTEGRA1:def 17 ;
hence upper_integral (r (#) f) = lower_integral (r (#) f) by A42; :: thesis: upper_integral (r (#) f) = r * (integral f)
upper_integral (r (#) f) = r * (upper_integral f) by A2, A42, INTEGRA1:def 17
.= r * (integral f) by INTEGRA1:def 18 ;
hence upper_integral (r (#) f) = r * (integral f) ; :: thesis: verum

end;

end;

end;

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

end;

hence ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) by A3, A4, INTEGRA1:def 17, INTEGRA1:def 18; :: thesis: verum