let n be Element of NAT ; :: thesis: for r being Real
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let r be Real; :: thesis: for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let f be PartFunc of REAL ,(REAL n); :: thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) ) )
assume that
A1: A c= dom f and
A2: f is_integrable_on A and
A3: f | A is bounded ; :: thesis: ( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )

A4: now

let i be Element of NAT ; :: thesis: A c= dom ((proj i,n) * f)
dom (proj i,n) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj i,n) ;
hence A c= dom ((proj i,n) * f) by A1, RELAT_1:46; :: thesis: verum

end;

A5: for i being Element of NAT st i in Seg n holds
integral (r (#) ((proj i,n) * f)),A = r * (integral ((proj i,n) * f),A)

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies integral (r (#) ((proj i,n) * f)),A = r * (integral ((proj i,n) * f),A) )
assume A6: i in Seg n ; :: thesis: integral (r (#) ((proj i,n) * f)),A = r * (integral ((proj i,n) * f),A)
((proj i,n) * f) | A = (proj i,n) * (f | A) by Lm6;
then A7: ((proj i,n) * f) | A is bounded by A3, A6, Def15;
A8: A c= dom ((proj i,n) * f) by A4;
(proj i,n) * f is_integrable_on A by A2, A6, Def16;
hence integral (r (#) ((proj i,n) * f)),A = r * (integral ((proj i,n) * f),A) by A7, A8, INTEGRA6:9; :: thesis: verum

end;

A9: for i being Element of NAT st i in Seg n holds
(r * (integral f,A)) . i = r * (integral ((proj i,n) * f),A)

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (r * (integral f,A)) . i = r * (integral ((proj i,n) * f),A) )
assume i in Seg n ; :: thesis: (r * (integral f,A)) . i = r * (integral ((proj i,n) * f),A)
then r * ((integral f,A) . i) = r * (integral ((proj i,n) * f),A) by Def17;
hence (r * (integral f,A)) . i = r * (integral ((proj i,n) * f),A) by RVSUM_1:67; :: thesis: verum

end;

A10: for i being Element of NAT st i in Seg n holds
(integral (r (#) f),A) . i = (r * (integral f,A)) . i

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (integral (r (#) f),A) . i = (r * (integral f,A)) . i )
A11: integral (r (#) ((proj i,n) * f)),A = integral ((proj i,n) * (r (#) f)),A by Th16;
assume A12: i in Seg n ; :: thesis: (integral (r (#) f),A) . i = (r * (integral f,A)) . i
then ( (integral (r (#) f),A) . i = integral ((proj i,n) * (r (#) f)),A & (r * (integral f,A)) . i = r * (integral ((proj i,n) * f),A) ) by A9, Def17;
hence (integral (r (#) f),A) . i = (r * (integral f,A)) . i by A5, A12, A11; :: thesis: verum

end;

for i being Element of NAT st i in Seg n holds
(proj i,n) * (r (#) f) is_integrable_on A

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj i,n) * (r (#) f) is_integrable_on A )
assume A13: i in Seg n ; :: thesis: (proj i,n) * (r (#) f) is_integrable_on A
((proj i,n) * f) | A = (proj i,n) * (f | A) by Lm6;
then A14: ((proj i,n) * f) | A is bounded by A3, A13, Def15;
A15: A c= dom ((proj i,n) * f) by A4;
(proj i,n) * f is_integrable_on A by A2, A13, Def16;
then r (#) ((proj i,n) * f) is_integrable_on A by A14, A15, INTEGRA6:9;
hence (proj i,n) * (r (#) f) is_integrable_on A by Th16; :: thesis: verum

end;

hence r (#) f is_integrable_on A by Def16; :: thesis: integral (r (#) f),A = r * (integral f,A)
A16: dom (integral (r (#) f),A) = Seg n by EUCLID:3;
then dom (integral (r (#) f),A) = dom (r * (integral f,A)) by EUCLID:3;
hence integral (r (#) f),A = r * (integral f,A) by A10, A16, PARTFUN1:34; :: thesis: verum