let Y be RealNormSpace; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A, the carrier of Y; :: thesis:
let E be Point of Y; :: thesis:
assume AS1: rng f = {E} ; :: thesis:
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 )

let k be Nat; :: thesis:
defpred S₁[ 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 S₁[i,x]

end;

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
S₁[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 )

let i be Nat; :: thesis:
assume i in dom (S . k) ; :: thesis:
then i in Seg (len (S . k)) by FINSEQ_1:def 3;
then B44: i in Seg (len (T . k)) by INTEGR18:def 1;
then i in dom (T . k) by FINSEQ_1:def 3;
then consider c being Point of Y such that
B42: ( c in rng (f | (divset ((T . k),i))) & (S . k) . i = (vol (divset ((T . k),i))) * c ) by INTEGR18:def 1;
c in rng f by B42, TARSKI:def 3, RELAT_1:70;
then B43: c = E by AS1, TARSKI:def 1;
q . i = vol (divset ((T . k),i)) by A18, B44;
hence ex r being Real st
( r = q . i & (S . k) . i = r * E ) by B42, B43; :: thesis:

end;

end;

let p be Real; :: thesis:
assume A3: 0 < p ; :: thesis:
reconsider k = 0 as Nat ;
take k = k; :: thesis:
let n be Nat; :: thesis:
assume k <= n ; :: thesis:
thus ||.(((middle_sum (f,S)) . n) - I).|| < p by A3, NORMSP_1:6, A1; :: thesis:

end;

end;