let n be Element of NAT ; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,(REAL n); :: thesis:
assume A1: f is bounded ; :: thesis:

hereby :: thesis:

reconsider I = integral f as Element of REAL n ;
assume A2: f is integrable ; :: thesis:
take I = I; :: thesis:
thus 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 ) by A1, A2, Th11; :: thesis:

end;

now :: thesis:

assume ex I being Element of REAL n st
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 ) ; :: thesis:
then consider I being Element of REAL n such that
A3: 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 ) ;

now :: thesis:

let i be Element of NAT ; :: thesis:
reconsider Ii = I . i as Element of REAL by XREAL_0:def 1;
assume A4: i in Seg n ; :: thesis:

A5: now :: thesis:

set x = I;
let T be DivSequence of A; :: thesis:
let Si be middle_volume_Sequence of (proj (i,n)) * f,T; :: thesis:
defpred S₁[ Element of NAT , set ] means ex H, z being FinSequence st
( H = T . $1 & z = $2 & len z = len H & ( for j being Element of NAT st j in dom H holds
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . $1),j))) & (Si . $1) . j = (vol (divset ((T . $1),j))) * ((((proj (i,n)) * f) | (divset ((T . $1),j))) . tji) & rji = (f | (divset ((T . $1),j))) . tji & z . j = (vol (divset ((T . $1),j))) * rji ) ) );
reconsider xs = I as Element of REAL n ;
A6: for k being Element of NAT ex y being Element of (REAL n) * st S₁[k,y]

proof

let k be Element of NAT ; :: thesis:
reconsider Tk = T . k as FinSequence ;
defpred S₂[ Nat, set ] means ex j being Element of NAT st
( $1 = j & ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & $2 = (vol (divset ((T . k),j))) * rji ) );
A7: for j being Nat st j in Seg (len Tk) holds
ex x being Element of REAL n st S₂[j,x]

proof

dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then A8: rng f c= dom (proj (i,n)) ;
let j0 be Nat; :: thesis:
assume A9: j0 in Seg (len Tk) ; :: thesis:
then reconsider j = j0 as Element of NAT ;
j in dom Tk by A9, FINSEQ_1:def 3;
then consider r being Element of REAL such that
A10: r in rng (((proj (i,n)) * f) | (divset ((T . k),j))) and
A11: (Si . k) . j = r * (vol (divset ((T . k),j))) by Def1;
consider tji being object such that
A12: tji in dom (((proj (i,n)) * f) | (divset ((T . k),j))) and
A13: r = (((proj (i,n)) * f) | (divset ((T . k),j))) . tji by A10, FUNCT_1:def 3;
tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A12, RELAT_1:61;
then reconsider tji = tji as Element of REAL ;
A14: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A8, RELAT_1:27
.= dom (((proj (i,n)) * f) | (divset ((T . k),j))) by RELAT_1:61 ;
then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A12, FUNCT_1:3;
then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of REAL n ;
reconsider x = (vol (divset ((T . k),j))) * rji as Element of REAL n ;
take x ; :: thesis:
thus S₂[j0,x] by A11, A12, A13, A14; :: thesis:

end;

consider p being FinSequence of REAL n such that
A15: ( dom p = Seg (len Tk) & ( for j being Nat st j in Seg (len Tk) holds
S₂[j,p . j] ) ) from FINSEQ_1:sch 5(A7);
reconsider x = p as Element of (REAL n) * by FINSEQ_1:def 11;
take x ; :: thesis:

A16: now :: thesis:

let jj0 be Element of NAT ; :: thesis:
reconsider j0 = jj0 as Nat ;
A17: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
assume jj0 in dom Tk ; :: thesis:
then S₂[j0,p . j0] by A15, A17;
hence ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ; :: thesis:

end;

len p = len Tk by A15, FINSEQ_1:def 3;
hence S₁[k,x] by A16; :: thesis:

end;

consider S being sequence of ((REAL n) *) such that
A18: for x being Element of NAT holds S₁[x,S . x] from FUNCT_2:sch 3(A6);
for k being Element of NAT holds S . k is middle_volume of f,T . k

proof

let k be Element of NAT ; :: thesis:
consider H, z being FinSequence such that
A19: ( H = T . k & z = S . k & len H = len z ) and
A20: for j being Element of NAT st j in dom H holds
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A18;

A21: now :: thesis:

let x be Nat; :: thesis:
assume A22: x in dom H ; :: thesis:
then reconsider j = x as Element of NAT ;
consider rji being Element of REAL n, tji being Element of REAL such that
A23: tji in dom (f | (divset ((T . k),j))) and
(Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) and
A24: rji = (f | (divset ((T . k),j))) . tji and
A25: z . j = (vol (divset ((T . k),j))) * rji by A20, A22;
take rji = rji; :: thesis:
thus rji in rng (f | (divset ((T . k),x))) by A23, A24, FUNCT_1:3; :: thesis:
thus z . x = (vol (divset ((T . k),x))) * rji by A25; :: thesis:

end;

thus S . k is middle_volume of f,T . k by A19, A21, Def5; :: thesis:

end;

then reconsider S = S as middle_volume_Sequence of f,T by Def7;
set seq = middle_sum (f,S);
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) ;
assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
then ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3;
then consider rseqi being Real_Sequence such that
A26: for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A4, REAL_NS1:11;
for k being Element of NAT holds rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k

proof

let k be Element of NAT ; :: thesis:
consider H, z being FinSequence such that
A27: H = T . k and
A28: z = S . k and
A29: len H = len z and
A30: for j being Element of NAT st j in dom H holds
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A18;
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng (S . k) c= dom (proj (i,n)) ;
then A31: dom ((proj (i,n)) * (S . k)) = dom (S . k) by RELAT_1:27
.= Seg (len H) by A28, A29, FINSEQ_1:def 3
.= Seg (len (Si . k)) by A27, Def1
.= dom (Si . k) by FINSEQ_1:def 3 ;
A32: for j being Nat st j in dom ((proj (i,n)) * (S . k)) holds
((proj (i,n)) * (S . k)) . j = (Si . k) . j

proof

let j0 be Nat; :: thesis:
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then A33: rng f c= dom (proj (i,n)) ;
assume A34: j0 in dom ((proj (i,n)) * (S . k)) ; :: thesis:
then j0 in Seg (len (Si . k)) by A31, FINSEQ_1:def 3;
then j0 in Seg (len H) by A27, Def1;
then j in dom H by FINSEQ_1:def 3;
then consider rji being Element of REAL n, tji being Element of REAL such that
A35: tji in dom (f | (divset ((T . k),j))) and
A36: (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) and
A37: rji = (f | (divset ((T . k),j))) . tji and
A38: z . j = (vol (divset ((T . k),j))) * rji by A30;
A39: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A33, RELAT_1:27
.= dom (((proj (i,n)) * f) | (divset ((T . k),j))) by RELAT_1:61 ;
then tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A35, RELAT_1:61;
then A40: tji in dom ((proj (i,n)) * f) by XBOOLE_0:def 4;
A41: (((proj (i,n)) * f) | (divset ((T . k),j))) . tji = ((proj (i,n)) * f) . tji by A35, A39, FUNCT_1:47
.= (proj (i,n)) . (f . tji) by A40, FUNCT_1:12
.= (proj (i,n)) . rji by A35, A37, FUNCT_1:47 ;
((proj (i,n)) * (S . k)) . j = (proj (i,n)) . ((S . k) . j) by A34, FUNCT_1:12
.= ((vol (divset ((T . k),j))) * rji) . i by A28, A38, PDIFF_1:def 1
.= (vol (divset ((T . k),j))) * (rji . i) by RVSUM_1:44
.= (Si . k) . j by A36, A41, PDIFF_1:def 1 ;
hence ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 ; :: thesis:

end;

consider Fi being FinSequence of REAL such that
A42: Fi = (proj (i,n)) * (S . k) and
A43: (middle_sum (f,(S . k))) . i = Sum Fi by A4, Def6;
thus rseqi . k = (xseq . k) . i by A26
.= Sum Fi by A43, Def8
.= middle_sum (((proj (i,n)) * f),(Si . k)) by A31, A32, A42, FINSEQ_1:13
.= (middle_sum (((proj (i,n)) * f),Si)) . k by Def4 ; :: thesis:

end;

hence ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) by A26, FUNCT_2:63; :: thesis:

end;

(proj (i,n)) * f is bounded by A1, A4;
hence (proj (i,n)) * f is integrable by A5, Th10; :: thesis:

end;

hence f is integrable ; :: thesis:

end;

hence ( ex I being Element of REAL n st
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 ) implies f is integrable ) ; :: thesis: