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) )
f is upper_integrable by A2, INTEGRA1:def 17;
then A3: rng (upper_sum_set f) is bounded_below by INTEGRA1:def 13;
f is lower_integrable by A2, INTEGRA1:def 17;
then A4: rng (lower_sum_set f) is bounded_above by INTEGRA1:def 14;
A5: dom (upper_sum_set f) = divs A by INTEGRA1:def 11;
then A6: upper_sum_set f is total by PARTFUN1:def 4;
A7: dom (lower_sum_set f) = divs A by INTEGRA1:def 12;
then A8: lower_sum_set f is total by PARTFUN1:def 4;
A9: not rng (lower_sum_set f) is empty by A7, RELAT_1:65;
A10: not rng (upper_sum_set f) is empty by A5, RELAT_1:65;

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;
A15: D in dom (upper_sum_set f) by A14, INTEGRA1:def 11;
D in dom (upper_sum_set (r (#) f)) by A14, INTEGRA1:def 11;
then (upper_sum_set (r (#) f)) . D = upper_sum (r (#) f),D by INTEGRA1:def 11
.= r * (upper_sum f,D) by A1, A12, Th27
.= r * ((upper_sum_set f) . D) by A15, INTEGRA1:def 11
.= (r (#) (upper_sum_set f)) . D by A6, A14, RFUNCT_1:73 ;
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 INTEGRA1:def 11
.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;
divs A = dom (upper_sum_set (r (#) f)) by INTEGRA1:def 11;
then upper_sum_set (r (#) f) = r (#) (upper_sum_set f) by A16, A13, FUNCT_1:9;
then A17: upper_integral (r (#) f) = lower_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def 15
.= lower_bound (r ** (rng (upper_sum_set f))) by A6, Th17
.= r * (lower_bound (rng (upper_sum_set f))) by A10, A3, A12, Th15
.= r * (upper_integral f) by INTEGRA1:def 15 ;
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;
A20: D in dom (lower_sum_set f) by A19, INTEGRA1:def 12;
D in dom (lower_sum_set (r (#) f)) by A19, INTEGRA1:def 12;
then (lower_sum_set (r (#) f)) . D = lower_sum (r (#) f),D by INTEGRA1:def 12
.= r * (lower_sum f,D) by A1, A12, Th29
.= r * ((lower_sum_set f) . D) by A20, INTEGRA1:def 12
.= (r (#) (lower_sum_set f)) . D by A8, A19, RFUNCT_1:73 ;
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 INTEGRA1:def 12
.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;
divs A = dom (lower_sum_set (r (#) f)) by INTEGRA1:def 12;
then lower_sum_set (r (#) f) = r (#) (lower_sum_set f) by A21, A18, FUNCT_1:9;
then lower_integral (r (#) f) = upper_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def 16
.= upper_bound (r ** (rng (lower_sum_set f))) by A8, Th17
.= r * (upper_bound (rng (lower_sum_set f))) by A4, A9, A12, 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 A17; :: thesis: upper_integral (r (#) f) = r * (integral f)
thus upper_integral (r (#) f) = r * (integral f) by A17, INTEGRA1:def 18; :: 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;
A25: D in dom (lower_sum_set f) by A24, INTEGRA1:def 12;
D in dom (upper_sum_set (r (#) f)) by A24, INTEGRA1:def 11;
then (upper_sum_set (r (#) f)) . D = upper_sum (r (#) f),D by INTEGRA1:def 11
.= r * (lower_sum f,D) by A1, A22, Th30
.= r * ((lower_sum_set f) . D) by A25, INTEGRA1:def 12
.= (r (#) (lower_sum_set f)) . D by A8, A24, RFUNCT_1:73 ;
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 INTEGRA1:def 12
.= dom (r (#) (lower_sum_set f)) by VALUED_1:def 5 ;
divs A = dom (upper_sum_set (r (#) f)) by INTEGRA1:def 11;
then upper_sum_set (r (#) f) = r (#) (lower_sum_set f) by A26, A23, FUNCT_1:9;
then A27: upper_integral (r (#) f) = lower_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def 15
.= lower_bound (r ** (rng (lower_sum_set f))) by A8, Th17
.= r * (upper_bound (rng (lower_sum_set f))) by A4, A9, A22, Th14
.= r * (lower_integral f) by INTEGRA1:def 16 ;
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;
A30: D in dom (upper_sum_set f) by A29, INTEGRA1:def 11;
D in dom (lower_sum_set (r (#) f)) by A29, INTEGRA1:def 12;
then (lower_sum_set (r (#) f)) . D = lower_sum (r (#) f),D by INTEGRA1:def 12
.= r * (upper_sum f,D) by A1, A22, Th28
.= r * ((upper_sum_set f) . D) by A30, INTEGRA1:def 11
.= (r (#) (upper_sum_set f)) . D by A6, A29, RFUNCT_1:73 ;
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 INTEGRA1:def 11
.= dom (r (#) (upper_sum_set f)) by VALUED_1:def 5 ;
divs A = dom (lower_sum_set (r (#) f)) by INTEGRA1:def 12;
then lower_sum_set (r (#) f) = r (#) (upper_sum_set f) by A31, A28, FUNCT_1:9;
then lower_integral (r (#) f) = upper_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def 16
.= upper_bound (r ** (rng (upper_sum_set f))) by A6, Th17
.= r * (lower_bound (rng (upper_sum_set f))) by A10, A3, A22, 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 A27; :: thesis: upper_integral (r (#) f) = r * (integral f)
upper_integral (r (#) f) = r * (upper_integral f) by A2, A27, INTEGRA1:def 17
.= r * (integral f) by INTEGRA1:def 18 ;
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:87;
then rng (lower_sum_set (r (#) f)) is bounded_above by INTEGRA1:15;
then A34: r (#) f is lower_integrable by INTEGRA1:def 14;
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:88;
then rng (upper_sum_set (r (#) f)) is bounded_below by INTEGRA1:13;
then r (#) f is upper_integrable by INTEGRA1:def 13;
hence ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) by A34, A11, INTEGRA1:def 17, INTEGRA1:def 18; :: thesis: verum