let n be Element of NAT ; 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; 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; 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); ( 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
; ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
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 ;
( 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
;
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;
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 ;
( i in Seg n implies (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) )
assume
i in Seg n
;
(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;
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 ;
( 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
;
(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;
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 ;
( i in Seg n implies (proj (i,n)) * (r (#) f) is_integrable_on A )
assume A13:
i in Seg n
;
(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;
verum
end;
hence
r (#) f is_integrable_on A
; 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; verum