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;

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

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

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

proof

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;

A9: 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 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

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;

A13: 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 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;

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

proof

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;

A17: 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 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

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;

A21: 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 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;

end;

end;

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

proof

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)) . D

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

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
(r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

proof

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;

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 ; :: thesis: verum

end;

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
(r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D

proof

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;

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 ; :: thesis: verum

end;

end;

end;

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 ; :: 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 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

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)) . D

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

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
(r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

proof

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;

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 ; :: thesis: verum

end;

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
(r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D

proof

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;

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 ; :: thesis: verum

end;

end;

end;

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 ; :: 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 A24, A5, INTEGRA1:def 16, INTEGRA1:def 17; :: thesis: verum