let n be Element of NAT ; :: thesis: for r being Real
for A being non empty 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 non empty 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 non empty 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 :: thesis: for i being Element of NAT holds A c= dom ((proj (i,n)) * f)

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:27; :: 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;
A8: A c= dom ((proj (i,n)) * f) by A4;
(proj (i,n)) * f is_integrable_on A by A2, A6;
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:45; :: 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;
A15: A c= dom ((proj (i,n)) * f) by A4;
(proj (i,n)) * f is_integrable_on A by A2, A13;
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 ; :: thesis: integral ((r (#) f),A) = r * (integral (f,A))
A16: dom (integral ((r (#) f),A)) = Seg n by FINSEQ_1:89;
then dom (integral ((r (#) f),A)) = dom (r * (integral (f,A))) by FINSEQ_1:89;
hence integral ((r (#) f),A) = r * (integral (f,A)) by A10, A16, PARTFUN1:5; :: thesis: verum