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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (REAL-NS n) 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 & (integral f) . i = lim rseqi )

integral f = x ;

hence ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A3, REAL_NS1:11; :: thesis: verum

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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (REAL-NS n) 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 & (integral f) . i = lim rseqi )

proof

reconsider x = integral f as Point of (REAL-NS n) by REAL_NS1:def 4;
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 & (integral f) . i = lim rseqi ) )

reconsider pjinf = (proj (i,n)) * f as Function of A,REAL ;

defpred S_{1}[ 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 S_{1}[x,y]

A5: for x being Element of NAT holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A4);

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 )

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 & (integral f) . i = lim rseqi )

A20: for k being Nat holds rseqi . k = (xseq . k) . i

( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )

A22: ( (proj (i,n)) * f is bounded & pjinf is integrable ) by A1, A19;

then lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, Th9;

hence for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) by A2, A19, A22, A20, Def14, Th9; :: thesis: verum

end;for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) )

reconsider pjinf = (proj (i,n)) * f as Function of A,REAL ;

defpred S

A4: for x being Element of NAT ex y being Element of REAL * st S

proof

consider F being sequence of (REAL *) such that
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S_{1}[x,y]

(proj (i,n)) * (S . x) is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S_{1}[x,y]
; :: thesis: verum

end;(proj (i,n)) * (S . x) is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S

A5: for x being Element of NAT holds S

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

for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
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;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

proof

then reconsider pjis = F as middle_volume_Sequence of pjinf,T by Def3;
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;

hence F . k is middle_volume of pjinf,T . k by A10, Def1; :: thesis: verum

end;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))) )

len Fk = len Tk
by A8, FINSEQ_1:def 3;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 A13, FUNCT_1:def 3;

t in (dom f) /\ (divset ((T . k),j)) by A15, RELAT_1:61;

then t in dom f by XBOOLE_0:def 4;

then A17: t in dom ((proj (i,n)) * f) by A11, RELAT_1:27;

A18: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61

.= (dom pjinf) /\ (divset ((T . k),j)) by A11, RELAT_1:27

.= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ;

(proj (i,n)) . r = (proj (i,n)) . (f . t) by A15, A16, FUNCT_1:47

.= ((proj (i,n)) * f) . t by A17, FUNCT_1:12

.= (pjinf | (divset ((T . k),j))) . t by A15, A18, FUNCT_1:47 ;

hence v in rng (pjinf | (divset ((T . k),j))) by A15, A18, FUNCT_1:3; :: thesis: Fk . j = v * (vol (divset ((T . k),j)))

thus Fk . j = (proj (i,n)) . ((S . k) . j) by A7, A9, A12, FUNCT_1:12

.= ((vol (divset ((T . k),j))) * r) . i by A14, PDIFF_1:def 1

.= (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;( 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 A13, FUNCT_1:def 3;

t in (dom f) /\ (divset ((T . k),j)) by A15, RELAT_1:61;

then t in dom f by XBOOLE_0:def 4;

then A17: t in dom ((proj (i,n)) * f) by A11, RELAT_1:27;

A18: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61

.= (dom pjinf) /\ (divset ((T . k),j)) by A11, RELAT_1:27

.= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ;

(proj (i,n)) . r = (proj (i,n)) . (f . t) by A15, A16, FUNCT_1:47

.= ((proj (i,n)) * f) . t by A17, FUNCT_1:12

.= (pjinf | (divset ((T . k),j))) . t by A15, A18, FUNCT_1:47 ;

hence v in rng (pjinf | (divset ((T . k),j))) by A15, A18, FUNCT_1:3; :: thesis: Fk . j = v * (vol (divset ((T . k),j)))

thus Fk . j = (proj (i,n)) . ((S . k) . j) by A7, A9, A12, FUNCT_1:12

.= ((vol (divset ((T . k),j))) * r) . i by A14, PDIFF_1:def 1

.= (vol (divset ((T . k),j))) * (r . i) by RVSUM_1:44

.= v * (vol (divset ((T . k),j))) by PDIFF_1:def 1 ; :: thesis: verum

hence F . k is middle_volume of pjinf,T . k by A10, Def1; :: thesis: verum

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 & (integral f) . i = lim rseqi )

A20: for k being Nat holds rseqi . k = (xseq . k) . i

proof

take
rseqi
; :: thesis: for k being Nat holds
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 A19, Def6;

rseqi . k = middle_sum (pjinf,(pjis . k)) by Def4

.= (middle_sum (f,(S . k))) . i by A5, A21

.= (xseq . k) . i by Def8 ;

hence rseqi . k = (xseq . k) . i ; :: thesis: verum

end;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 A19, Def6;

rseqi . k = middle_sum (pjinf,(pjis . k)) by Def4

.= (middle_sum (f,(S . k))) . i by A5, A21

.= (xseq . k) . i by Def8 ;

hence rseqi . k = (xseq . k) . i ; :: thesis: verum

( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )

A22: ( (proj (i,n)) * f is bounded & pjinf is integrable ) by A1, A19;

then lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, Th9;

hence for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) by A2, A19, A22, A20, Def14, Th9; :: thesis: verum

integral f = x ;

hence ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A3, REAL_NS1:11; :: thesis: verum