let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

let f be Function of A,(REAL n); :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

let S be middle_volume_Sequence of f,T; :: thesis: ( f is bounded & f is integrable & delta T is convergent & lim () = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) )
assume that
A1: ( f is bounded & f is integrable ) and
A2: ( delta T is convergent & lim () = 0 ) ; :: thesis: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
set seq = middle_sum (f,S);
set xs = integral f;
REAL n = the carrier of () by REAL_NS1:def 4;
then reconsider xseq = middle_sum (f,S) as sequence of (REAL n) ;
A3: for i being Nat st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & () . i = lim rseqi )
proof
let i be Nat; :: thesis: ( i in Seg n implies ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & () . i = lim rseqi ) )

reconsider pjinf = (proj (i,n)) * f as Function of A,REAL ;
defpred S1[ Element of NAT , set ] means \$2 = (proj (i,n)) * (S . \$1);
A4: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S1[x,y]
(proj (i,n)) * (S . x) is Element of REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S1[x,y] ; :: thesis: verum
end;
consider F being sequence of () such that
A5: for x being Element of NAT holds S1[x,F . x] from A6: for x being Element of NAT holds
( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL )
proof
let x be Element of NAT ; :: thesis: ( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL )
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng (S . x) c= dom (proj (i,n)) ;
then dom ((proj (i,n)) * (S . x)) = dom (S . x) by RELAT_1:27
.= Seg (len (S . x)) by FINSEQ_1:def 3 ;
hence ( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL ) ; :: thesis: verum
end;
for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
proof
let k be Element of NAT ; :: thesis: F . k is middle_volume of pjinf,T . k
reconsider Tk = T . k as FinSequence ;
reconsider Fk = F . k as FinSequence of REAL ;
A7: F . k = (proj (i,n)) * (S . k) by A5;
then A8: dom Fk = Seg (len (S . k)) by A6
.= Seg (len Tk) by Def5 ;
then A9: dom Fk = dom Tk by FINSEQ_1:def 3;
A10: now :: thesis: for j being Nat st j in dom Tk holds
ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
let j be Nat; :: thesis: ( j in dom Tk implies ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) )

dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then A11: rng f c= dom (proj (i,n)) ;
assume A12: j in dom Tk ; :: thesis: ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )

then consider r being Element of REAL n such that
A13: r in rng (f | (divset ((T . k),j))) and
A14: (S . k) . j = (vol (divset ((T . k),j))) * r by Def5;
reconsider v = (proj (i,n)) . r as Element of REAL ;
take v = v; :: thesis: ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
consider t being object such that
A15: t in dom (f | (divset ((T . k),j))) and
A16: r = (f | (divset ((T . k),j))) . t by ;
t in (dom f) /\ (divset ((T . k),j)) by ;
then t in dom f by XBOOLE_0:def 4;
then A17: t in dom ((proj (i,n)) * f) by ;
A18: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom pjinf) /\ (divset ((T . k),j)) by
.= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ;
(proj (i,n)) . r = (proj (i,n)) . (f . t) by
.= ((proj (i,n)) * f) . t by
.= (pjinf | (divset ((T . k),j))) . t by ;
hence v in rng (pjinf | (divset ((T . k),j))) by ; :: thesis: Fk . j = v * (vol (divset ((T . k),j)))
thus Fk . j = (proj (i,n)) . ((S . k) . j) by
.= ((vol (divset ((T . k),j))) * r) . i by
.= (vol (divset ((T . k),j))) * (r . i) by RVSUM_1:44
.= v * (vol (divset ((T . k),j))) by PDIFF_1:def 1 ; :: thesis: verum
end;
len Fk = len Tk by ;
hence F . k is middle_volume of pjinf,T . k by ; :: thesis: verum
end;
then reconsider pjis = F as middle_volume_Sequence of pjinf,T by Def3;
reconsider rseqi = middle_sum (pjinf,pjis) as Real_Sequence ;
assume A19: i in Seg n ; :: thesis: ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & () . i = lim rseqi )

A20: for k being Nat holds rseqi . k = (xseq . k) . i
proof
let k be Nat; :: thesis: rseqi . k = (xseq . k) . i
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A21: ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * (S . k) & (middle_sum (f,(S . k))) . i = Sum Fi ) by ;
rseqi . k = middle_sum (pjinf,(pjis . k)) by Def4
.= (middle_sum (f,(S . k))) . i by
.= (xseq . k) . i by Def8 ;
hence rseqi . k = (xseq . k) . i ; :: thesis: verum
end;
take rseqi ; :: thesis: for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & () . i = lim rseqi )

A22: ( (proj (i,n)) * f is bounded & pjinf is integrable ) by ;
then lim (middle_sum (pjinf,pjis)) = integral pjinf by ;
hence for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & () . i = lim rseqi ) by A2, A19, A22, A20, Def14, Th9; :: thesis: verum
end;
reconsider x = integral f as Point of () by REAL_NS1:def 4;
integral f = x ;
hence ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by ; :: thesis: verum