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) st f is bounded holds

( f is integrable iff 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 ) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,(REAL n) st f is bounded holds

( f is integrable iff 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 ) )

let f be Function of A,(REAL n); :: thesis: ( f is bounded implies ( f is integrable iff 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 ) ) )

assume A1: f is bounded ; :: thesis: ( f is integrable iff 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 ) )

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: verum

for f being Function of A,(REAL n) st f is bounded holds

( f is integrable iff 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 ) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,(REAL n) st f is bounded holds

( f is integrable iff 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 ) )

let f be Function of A,(REAL n); :: thesis: ( f is bounded implies ( f is integrable iff 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 ) ) )

assume A1: f is bounded ; :: thesis: ( f is integrable iff 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 ) )

hereby :: thesis: ( 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 )

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 )

reconsider I = integral f as Element of REAL n ;

assume A2: f is integrable ; :: thesis: 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 )

take I = I; :: thesis: 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 )

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: verum

end;assume A2: f is integrable ; :: thesis: 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 )

take I = I; :: thesis: 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 )

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: verum

now :: thesis: ( 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 )

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 )

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: f is integrable

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

end;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: f is integrable

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: for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is integrable

hence
f is integrable
; :: thesis: verum(proj (i,n)) * f is integrable

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj (i,n)) * f is integrable )

reconsider Ii = I . i as Element of REAL by XREAL_0:def 1;

assume A4: i in Seg n ; :: thesis: (proj (i,n)) * f is integrable

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

end;reconsider Ii = I . i as Element of REAL by XREAL_0:def 1;

assume A4: i in Seg n ; :: thesis: (proj (i,n)) * f is integrable

A5: now :: thesis: for T being DivSequence of A

for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )

(proj (i,n)) * f is bounded
by A1, A4;for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )

set x = I;

let T be DivSequence of A; :: thesis: for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )

let Si be middle_volume_Sequence of (proj (i,n)) * f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) )

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

A18: for x being Element of NAT holds S_{1}[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

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: ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )

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

end;let T be DivSequence of A; :: thesis: for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )

let Si be middle_volume_Sequence of (proj (i,n)) * f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) )

defpred S

( 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

proof

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

reconsider Tk = T . k as FinSequence ;

defpred S_{2}[ 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_{2}[j,x]

A15: ( dom p = Seg (len Tk) & ( for j being Nat st j in Seg (len Tk) holds

S_{2}[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: S_{1}[k,x]

hence S_{1}[k,x]
by A16; :: thesis: verum

end;reconsider Tk = T . k as FinSequence ;

defpred S

( $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

proof

consider p being FinSequence of REAL n such that
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: ( j0 in Seg (len Tk) implies ex x being Element of REAL n st S_{2}[j0,x] )

assume A9: j0 in Seg (len Tk) ; :: thesis: ex x being Element of REAL n st S_{2}[j0,x]

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: S_{2}[j0,x]

thus S_{2}[j0,x]
by A11, A12, A13, A14; :: thesis: verum

end;then A8: rng f c= dom (proj (i,n)) ;

let j0 be Nat; :: thesis: ( j0 in Seg (len Tk) implies ex x being Element of REAL n st S

assume A9: j0 in Seg (len Tk) ; :: thesis: ex x being Element of REAL n st S

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: S

thus S

A15: ( dom p = Seg (len Tk) & ( for j being Nat st j in Seg (len Tk) holds

S

reconsider x = p as Element of (REAL n) * by FINSEQ_1:def 11;

take x ; :: thesis: S

A16: now :: thesis: for jj0 being Element of NAT st jj0 in dom Tk holds

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 )

len p = len Tk
by A15, FINSEQ_1:def 3;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 )

let jj0 be Element of NAT ; :: thesis: ( jj0 in dom Tk implies 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 ) )

reconsider j0 = jj0 as Nat ;

A17: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;

assume jj0 in dom Tk ; :: thesis: 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 )

then S_{2}[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: verum

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

reconsider j0 = jj0 as Nat ;

A17: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;

assume jj0 in dom Tk ; :: thesis: 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 )

then S

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: verum

hence S

A18: for x being Element of NAT holds S

for k being Element of NAT holds S . k is middle_volume of f,T . k

proof

then reconsider S = S as middle_volume_Sequence of f,T by Def7;
let k be Element of NAT ; :: thesis: S . k is middle_volume of f,T . k

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;

end;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: for x being Nat st x in dom H holds

ex rji being Element of REAL n st

( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )

thus
S . k is middle_volume of f,T . k
by A19, A21, Def5; :: thesis: verumex rji being Element of REAL n st

( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )

let x be Nat; :: thesis: ( x in dom H implies ex rji being Element of REAL n st

( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji ) )

assume A22: x in dom H ; :: thesis: ex rji being Element of REAL n st

( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )

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: ( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )

thus rji in rng (f | (divset ((T . k),x))) by A23, A24, FUNCT_1:3; :: thesis: z . x = (vol (divset ((T . k),x))) * rji

thus z . x = (vol (divset ((T . k),x))) * rji by A25; :: thesis: verum

end;( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji ) )

assume A22: x in dom H ; :: thesis: ex rji being Element of REAL n st

( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )

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: ( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )

thus rji in rng (f | (divset ((T . k),x))) by A23, A24, FUNCT_1:3; :: thesis: z . x = (vol (divset ((T . k),x))) * rji

thus z . x = (vol (divset ((T . k),x))) * rji by A25; :: thesis: verum

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: ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )

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

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: verum
let k be Element of NAT ; :: thesis: rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k

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

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: verum

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

consider Fi being FinSequence of REAL such that
let j0 be Nat; :: thesis: ( j0 in dom ((proj (i,n)) * (S . k)) implies ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 )

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: ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0

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: verum

end;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: ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0

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: verum

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: verum

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

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: verum