let Y be RealNormSpace; for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of Y
for E being Point of Y st rng f = {E} holds
( f is integrable & integral f = (vol A) * E )
let A be non empty closed_interval Subset of REAL; for f being Function of A, the carrier of Y
for E being Point of Y st rng f = {E} holds
( f is integrable & integral f = (vol A) * E )
let f be Function of A, the carrier of Y; for E being Point of Y st rng f = {E} holds
( f is integrable & integral f = (vol A) * E )
let E be Point of Y; ( rng f = {E} implies ( f is integrable & integral f = (vol A) * E ) )
assume AS1:
rng f = {E}
; ( f is integrable & integral f = (vol A) * E )
reconsider I = (vol A) * E as Point of Y ;
P1:
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
proof
let T be
DivSequence of
A;
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )let S be
middle_volume_Sequence of
f,
T;
( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
assume
(
delta T is
convergent &
lim (delta T) = 0 )
;
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
set s =
middle_sum (
f,
S);
A1:
for
k being
Nat holds
(middle_sum (f,S)) . k = I
proof
let k be
Nat;
(middle_sum (f,S)) . k = I
defpred S1[
Nat,
set ]
means $2
= vol (divset ((T . k),$1));
A14:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
x being
Element of
REAL st
S1[
i,
x]
consider q being
FinSequence of
REAL such that A18:
(
dom q = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S1[
i,
q . i] ) )
from FINSEQ_1:sch 5(A14);
B7:
Sum q = vol A
by INTEGR20:6, A18;
len q = len (T . k)
by A18, FINSEQ_1:def 3;
then B8:
len (S . k) = len q
by INTEGR18:def 1;
B40:
for
i being
Nat st
i in dom (S . k) holds
ex
r being
Real st
(
r = q . i &
(S . k) . i = r * E )
(middle_sum (f,S)) . k = middle_sum (
f,
(S . k))
by INTEGR18:def 4;
hence
(middle_sum (f,S)) . k = I
by B40, B7, B8, INTEGR20:7;
verum
end;
hence
middle_sum (
f,
S) is
convergent
;
lim (middle_sum (f,S)) = I
hence
lim (middle_sum (f,S)) = I
by A2, NORMSP_1:def 7;
verum
end;
hence
f is integrable
; integral f = (vol A) * E
hence
integral f = (vol A) * E
by P1, INTEGR18:def 6; verum