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

( f is integrable iff ex I being Element of COMPLEX 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,COMPLEX; :: thesis: ( f is bounded implies ( f is integrable iff ex I being Element of COMPLEX 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 COMPLEX 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

( f is integrable iff ex I being Element of COMPLEX 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,COMPLEX; :: thesis: ( f is bounded implies ( f is integrable iff ex I being Element of COMPLEX 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 COMPLEX 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 COMPLEX 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 COMPLEX ;

assume A2: f is integrable ; :: thesis: ex I being Element of COMPLEX 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, Th14; :: thesis: verum

end;assume A2: f is integrable ; :: thesis: ex I being Element of COMPLEX 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, Th14; :: thesis: verum

now :: thesis: ( ex I being Element of COMPLEX 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 COMPLEX 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 COMPLEX 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 COMPLEX 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 ) ;

reconsider Ii = Re I as Element of REAL ;

reconsider Ic = Im I as Element of REAL ;

then A41: Re f is integrable by A4, INTEGR15:10;

then Im f is integrable by A42, INTEGR15:10;

hence f is integrable by A41; :: thesis: verum

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

reconsider Ii = Re I as Element of REAL ;

reconsider Ic = Im I as Element of REAL ;

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

for Si being middle_volume_Sequence of Re f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )

Re f is bounded
by A1, Th13;for Si being middle_volume_Sequence of Re f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )

set x = I;

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

( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )

let Si be middle_volume_Sequence of Re f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . $1),j))) & (Si . $1) . j = (vol (divset ((T . $1),j))) * (((Re 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 COMPLEX ;

A5: for k being Element of NAT ex y being Element of COMPLEX * st S_{1}[k,y]

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

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

set seq = middle_sum (f,S);

reconsider xseq = middle_sum (f,S) as sequence of COMPLEX ;

assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )

then A24: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3;

reconsider rseqi = Re (middle_sum (f,S)) as Real_Sequence ;

A25: for k being Element of NAT holds

( rseqi . k = Re (xseq . k) & rseqi is convergent & Re xs = lim rseqi ) by A24, COMSEQ_3:41, COMSEQ_3:def 5;

for k being Element of NAT holds rseqi . k = (middle_sum ((Re f),Si)) . k

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

( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )

let Si be middle_volume_Sequence of Re f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . $1),j))) & (Si . $1) . j = (vol (divset ((T . $1),j))) * (((Re 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 COMPLEX ;

A5: for k being Element of NAT ex y being Element of COMPLEX * st S

proof

consider S being sequence of (COMPLEX *) such that
let k be Element of NAT ; :: thesis: ex y being Element of COMPLEX * 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & $2 = (vol (divset ((T . k),j))) * rji ) );

A6: for j being Nat st j in Seg (len Tk) holds

ex x being Element of COMPLEX st S_{2}[j,x]

A13: ( 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(A6);

reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;

take x ; :: thesis: S_{1}[k,x]

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

end;reconsider Tk = T . k as FinSequence ;

defpred S

( $1 = j & ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & $2 = (vol (divset ((T . k),j))) * rji ) );

A6: for j being Nat st j in Seg (len Tk) holds

ex x being Element of COMPLEX st S

proof

consider p being FinSequence of COMPLEX such that
let j0 be Nat; :: thesis: ( j0 in Seg (len Tk) implies ex x being Element of COMPLEX st S_{2}[j0,x] )

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

then reconsider j = j0 as Element of NAT ;

j in dom Tk by A7, FINSEQ_1:def 3;

then consider r being Element of REAL such that

A8: r in rng ((Re f) | (divset ((T . k),j))) and

A9: (Si . k) . j = r * (vol (divset ((T . k),j))) by INTEGR15:def 1;

consider tji being object such that

A10: tji in dom ((Re f) | (divset ((T . k),j))) and

A11: r = ((Re f) | (divset ((T . k),j))) . tji by A8, FUNCT_1:def 3;

tji in (dom (Re f)) /\ (divset ((T . k),j)) by A10, RELAT_1:61;

then reconsider tji = tji as Element of REAL ;

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

.= (dom (Re f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 3

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

then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A10, FUNCT_1:3;

then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of COMPLEX ;

reconsider x = (vol (divset ((T . k),j))) * rji as Element of COMPLEX by XCMPLX_0:def 2;

take x ; :: thesis: S_{2}[j0,x]

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

end;assume A7: j0 in Seg (len Tk) ; :: thesis: ex x being Element of COMPLEX st S

then reconsider j = j0 as Element of NAT ;

j in dom Tk by A7, FINSEQ_1:def 3;

then consider r being Element of REAL such that

A8: r in rng ((Re f) | (divset ((T . k),j))) and

A9: (Si . k) . j = r * (vol (divset ((T . k),j))) by INTEGR15:def 1;

consider tji being object such that

A10: tji in dom ((Re f) | (divset ((T . k),j))) and

A11: r = ((Re f) | (divset ((T . k),j))) . tji by A8, FUNCT_1:def 3;

tji in (dom (Re f)) /\ (divset ((T . k),j)) by A10, RELAT_1:61;

then reconsider tji = tji as Element of REAL ;

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

.= (dom (Re f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 3

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

then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A10, FUNCT_1:3;

then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of COMPLEX ;

reconsider x = (vol (divset ((T . k),j))) * rji as Element of COMPLEX by XCMPLX_0:def 2;

take x ; :: thesis: S

thus S

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

S

reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;

take x ; :: thesis: S

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

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re 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 A13, FINSEQ_1:def 3;ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re 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 ;

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

assume jj0 in dom Tk ; :: thesis: ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re 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 A13, A15;

hence ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re 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))) * (((Re 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 ;

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

assume jj0 in dom Tk ; :: thesis: ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re 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

A16: 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 Def3;
let k be Element of NAT ; :: thesis: S . k is middle_volume of f,T . k

consider H, z being FinSequence such that

A17: ( H = T . k & z = S . k & len H = len z ) and

A18: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A16;

end;consider H, z being FinSequence such that

A17: ( H = T . k & z = S . k & len H = len z ) and

A18: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A16;

A19: now :: thesis: for x being Nat st x in dom H holds

ex rji being Element of COMPLEX st

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

thus
S . k is middle_volume of f,T . k
by A17, A19, Def1; :: thesis: verumex rji being Element of COMPLEX st

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

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

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

assume A20: x in dom H ; :: thesis: ex rji being Element of COMPLEX st

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

then reconsider j = x as Element of NAT ;

consider rji being Element of COMPLEX , tji being Element of REAL such that

A21: tji in dom (f | (divset ((T . k),j))) and

(Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) and

A22: rji = (f | (divset ((T . k),j))) . tji and

A23: z . j = (vol (divset ((T . k),j))) * rji by A18, A20;

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

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

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

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

assume A20: x in dom H ; :: thesis: ex rji being Element of COMPLEX st

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

then reconsider j = x as Element of NAT ;

consider rji being Element of COMPLEX , tji being Element of REAL such that

A21: tji in dom (f | (divset ((T . k),j))) and

(Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) and

A22: rji = (f | (divset ((T . k),j))) . tji and

A23: z . j = (vol (divset ((T . k),j))) * rji by A18, A20;

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

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

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

set seq = middle_sum (f,S);

reconsider xseq = middle_sum (f,S) as sequence of COMPLEX ;

assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )

then A24: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3;

reconsider rseqi = Re (middle_sum (f,S)) as Real_Sequence ;

A25: for k being Element of NAT holds

( rseqi . k = Re (xseq . k) & rseqi is convergent & Re xs = lim rseqi ) by A24, COMSEQ_3:41, COMSEQ_3:def 5;

for k being Element of NAT holds rseqi . k = (middle_sum ((Re f),Si)) . k

proof

hence
( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )
by A25, FUNCT_2:63; :: thesis: verum
let k be Element of NAT ; :: thesis: rseqi . k = (middle_sum ((Re f),Si)) . k

consider H, z being FinSequence such that

A26: H = T . k and

A27: z = S . k and

A28: len H = len z and

A29: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A16;

A30: dom (Re (S . k)) = dom (S . k) by COMSEQ_3:def 3

.= Seg (len H) by A27, A28, FINSEQ_1:def 3

.= Seg (len (Si . k)) by A26, INTEGR15:def 1

.= dom (Si . k) by FINSEQ_1:def 3 ;

A31: for j being Nat st j in dom (Re (S . k)) holds

(Re (S . k)) . j = (Si . k) . j

(Re (S . k)) . j0 = (Si . k) . j0 by A31;

thus rseqi . k = Re (xseq . k) by COMSEQ_3:def 5

.= Re (middle_sum (f,(S . k))) by Def4

.= middle_sum ((Re f),(Si . k)) by A30, A40, Th7, FUNCT_1:2

.= (middle_sum ((Re f),Si)) . k by INTEGR15:def 4 ; :: thesis: verum

end;consider H, z being FinSequence such that

A26: H = T . k and

A27: z = S . k and

A28: len H = len z and

A29: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A16;

A30: dom (Re (S . k)) = dom (S . k) by COMSEQ_3:def 3

.= Seg (len H) by A27, A28, FINSEQ_1:def 3

.= Seg (len (Si . k)) by A26, INTEGR15:def 1

.= dom (Si . k) by FINSEQ_1:def 3 ;

A31: for j being Nat st j in dom (Re (S . k)) holds

(Re (S . k)) . j = (Si . k) . j

proof

A40:
for j0 being object st j0 in dom (Re (S . k)) holds
let j0 be Nat; :: thesis: ( j0 in dom (Re (S . k)) implies (Re (S . k)) . j0 = (Si . k) . j0 )

reconsider j = j0 as Element of NAT by ORDINAL1:def 12;

assume A32: j0 in dom (Re (S . k)) ; :: thesis: (Re (S . k)) . j0 = (Si . k) . j0

then j0 in Seg (len (Si . k)) by A30, FINSEQ_1:def 3;

then j0 in Seg (len H) by A26, INTEGR15:def 1;

then j in dom H by FINSEQ_1:def 3;

then consider rji being Element of COMPLEX , tji being Element of REAL such that

A33: tji in dom (f | (divset ((T . k),j))) and

A34: (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) and

A35: rji = (f | (divset ((T . k),j))) . tji and

A36: z . j = (vol (divset ((T . k),j))) * rji by A29;

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

.= (dom (Re f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 3

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

then tji in (dom (Re f)) /\ (divset ((T . k),j)) by A33, RELAT_1:61;

then A38: tji in dom (Re f) by XBOOLE_0:def 4;

A39: ((Re f) | (divset ((T . k),j))) . tji = (Re f) . tji by A33, A37, FUNCT_1:47

.= Re (f . tji) by A38, COMSEQ_3:def 3

.= Re rji by A33, A35, FUNCT_1:47 ;

(Re (S . k)) . j = Re ((S . k) . j) by A32, COMSEQ_3:def 3

.= (Si . k) . j by A34, A39, Th1, A27, A36 ;

hence (Re (S . k)) . j0 = (Si . k) . j0 ; :: thesis: verum

end;reconsider j = j0 as Element of NAT by ORDINAL1:def 12;

assume A32: j0 in dom (Re (S . k)) ; :: thesis: (Re (S . k)) . j0 = (Si . k) . j0

then j0 in Seg (len (Si . k)) by A30, FINSEQ_1:def 3;

then j0 in Seg (len H) by A26, INTEGR15:def 1;

then j in dom H by FINSEQ_1:def 3;

then consider rji being Element of COMPLEX , tji being Element of REAL such that

A33: tji in dom (f | (divset ((T . k),j))) and

A34: (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) and

A35: rji = (f | (divset ((T . k),j))) . tji and

A36: z . j = (vol (divset ((T . k),j))) * rji by A29;

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

.= (dom (Re f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 3

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

then tji in (dom (Re f)) /\ (divset ((T . k),j)) by A33, RELAT_1:61;

then A38: tji in dom (Re f) by XBOOLE_0:def 4;

A39: ((Re f) | (divset ((T . k),j))) . tji = (Re f) . tji by A33, A37, FUNCT_1:47

.= Re (f . tji) by A38, COMSEQ_3:def 3

.= Re rji by A33, A35, FUNCT_1:47 ;

(Re (S . k)) . j = Re ((S . k) . j) by A32, COMSEQ_3:def 3

.= (Si . k) . j by A34, A39, Th1, A27, A36 ;

hence (Re (S . k)) . j0 = (Si . k) . j0 ; :: thesis: verum

(Re (S . k)) . j0 = (Si . k) . j0 by A31;

thus rseqi . k = Re (xseq . k) by COMSEQ_3:def 5

.= Re (middle_sum (f,(S . k))) by Def4

.= middle_sum ((Re f),(Si . k)) by A30, A40, Th7, FUNCT_1:2

.= (middle_sum ((Re f),Si)) . k by INTEGR15:def 4 ; :: thesis: verum

then A41: Re f is integrable by A4, INTEGR15:10;

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

for Si being middle_volume_Sequence of Im f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )

Im f is bounded
by A1, Th13;for Si being middle_volume_Sequence of Im f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )

set x = I;

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

( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )

let Si be middle_volume_Sequence of Im f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) )

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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . $1),j))) & (Si . $1) . j = (vol (divset ((T . $1),j))) * (((Im 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 COMPLEX ;

A43: for k being Element of NAT ex y being Element of COMPLEX * st S_{1}[k,y]

A54: for x being Element of NAT holds S_{1}[x,S . x]
from FUNCT_2:sch 3(A43);

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

set seq = middle_sum (f,S);

reconsider xseq = middle_sum (f,S) as sequence of COMPLEX ;

assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )

then A62: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3;

reconsider rseqi = Im (middle_sum (f,S)) as Real_Sequence ;

A63: for k being Element of NAT holds

( rseqi . k = Im (xseq . k) & rseqi is convergent & Im xs = lim rseqi ) by A62, COMSEQ_3:41, COMSEQ_3:def 6;

for k being Element of NAT holds rseqi . k = (middle_sum ((Im f),Si)) . k

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

( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )

let Si be middle_volume_Sequence of Im f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) )

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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . $1),j))) & (Si . $1) . j = (vol (divset ((T . $1),j))) * (((Im 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 COMPLEX ;

A43: for k being Element of NAT ex y being Element of COMPLEX * st S

proof

consider S being sequence of (COMPLEX *) such that
let k be Element of NAT ; :: thesis: ex y being Element of COMPLEX * 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & $2 = (vol (divset ((T . k),j))) * rji ) );

A44: for j being Nat st j in Seg (len Tk) holds

ex x being Element of COMPLEX st S_{2}[j,x]

A51: ( 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(A44);

reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;

take x ; :: thesis: S_{1}[k,x]

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

end;reconsider Tk = T . k as FinSequence ;

defpred S

( $1 = j & ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & $2 = (vol (divset ((T . k),j))) * rji ) );

A44: for j being Nat st j in Seg (len Tk) holds

ex x being Element of COMPLEX st S

proof

consider p being FinSequence of COMPLEX such that
let j0 be Nat; :: thesis: ( j0 in Seg (len Tk) implies ex x being Element of COMPLEX st S_{2}[j0,x] )

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

then reconsider j = j0 as Element of NAT ;

j in dom Tk by A45, FINSEQ_1:def 3;

then consider r being Element of REAL such that

A46: r in rng ((Im f) | (divset ((T . k),j))) and

A47: (Si . k) . j = r * (vol (divset ((T . k),j))) by INTEGR15:def 1;

consider tji being object such that

A48: tji in dom ((Im f) | (divset ((T . k),j))) and

A49: r = ((Im f) | (divset ((T . k),j))) . tji by A46, FUNCT_1:def 3;

tji in (dom (Im f)) /\ (divset ((T . k),j)) by A48, RELAT_1:61;

then reconsider tji = tji as Element of REAL ;

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

.= (dom (Im f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 4

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

then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A48, FUNCT_1:3;

then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of COMPLEX ;

reconsider x = (vol (divset ((T . k),j))) * rji as Element of COMPLEX by XCMPLX_0:def 2;

take x ; :: thesis: S_{2}[j0,x]

thus S_{2}[j0,x]
by A47, A48, A49, A50; :: thesis: verum

end;assume A45: j0 in Seg (len Tk) ; :: thesis: ex x being Element of COMPLEX st S

then reconsider j = j0 as Element of NAT ;

j in dom Tk by A45, FINSEQ_1:def 3;

then consider r being Element of REAL such that

A46: r in rng ((Im f) | (divset ((T . k),j))) and

A47: (Si . k) . j = r * (vol (divset ((T . k),j))) by INTEGR15:def 1;

consider tji being object such that

A48: tji in dom ((Im f) | (divset ((T . k),j))) and

A49: r = ((Im f) | (divset ((T . k),j))) . tji by A46, FUNCT_1:def 3;

tji in (dom (Im f)) /\ (divset ((T . k),j)) by A48, RELAT_1:61;

then reconsider tji = tji as Element of REAL ;

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

.= (dom (Im f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 4

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

then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A48, FUNCT_1:3;

then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of COMPLEX ;

reconsider x = (vol (divset ((T . k),j))) * rji as Element of COMPLEX by XCMPLX_0:def 2;

take x ; :: thesis: S

thus S

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

S

reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;

take x ; :: thesis: S

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

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im 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 A51, FINSEQ_1:def 3;ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im 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 ;

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

assume jj0 in dom Tk ; :: thesis: ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im 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 A51, A53;

hence ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im 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))) * (((Im 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 ;

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

assume jj0 in dom Tk ; :: thesis: ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im 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 COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im 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

A54: 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 Def3;
let k be Element of NAT ; :: thesis: S . k is middle_volume of f,T . k

consider H, z being FinSequence such that

A55: ( H = T . k & z = S . k & len H = len z ) and

A56: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A54;

end;consider H, z being FinSequence such that

A55: ( H = T . k & z = S . k & len H = len z ) and

A56: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A54;

A57: now :: thesis: for x being Nat st x in dom H holds

ex rji being Element of COMPLEX st

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

thus
S . k is middle_volume of f,T . k
by A55, A57, Def1; :: thesis: verumex rji being Element of COMPLEX st

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

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

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

assume A58: x in dom H ; :: thesis: ex rji being Element of COMPLEX st

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

then reconsider j = x as Element of NAT ;

consider rji being Element of COMPLEX , tji being Element of REAL such that

A59: tji in dom (f | (divset ((T . k),j))) and

(Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) and

A60: rji = (f | (divset ((T . k),j))) . tji and

A61: z . j = (vol (divset ((T . k),j))) * rji by A56, A58;

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

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

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

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

assume A58: x in dom H ; :: thesis: ex rji being Element of COMPLEX st

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

then reconsider j = x as Element of NAT ;

consider rji being Element of COMPLEX , tji being Element of REAL such that

A59: tji in dom (f | (divset ((T . k),j))) and

(Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) and

A60: rji = (f | (divset ((T . k),j))) . tji and

A61: z . j = (vol (divset ((T . k),j))) * rji by A56, A58;

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

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

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

set seq = middle_sum (f,S);

reconsider xseq = middle_sum (f,S) as sequence of COMPLEX ;

assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )

then A62: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3;

reconsider rseqi = Im (middle_sum (f,S)) as Real_Sequence ;

A63: for k being Element of NAT holds

( rseqi . k = Im (xseq . k) & rseqi is convergent & Im xs = lim rseqi ) by A62, COMSEQ_3:41, COMSEQ_3:def 6;

for k being Element of NAT holds rseqi . k = (middle_sum ((Im f),Si)) . k

proof

hence
( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )
by A63, FUNCT_2:63; :: thesis: verum
let k be Element of NAT ; :: thesis: rseqi . k = (middle_sum ((Im f),Si)) . k

consider H, z being FinSequence such that

A64: H = T . k and

A65: z = S . k and

A66: len H = len z and

A67: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A54;

A68: dom (Im (S . k)) = dom (S . k) by COMSEQ_3:def 4

.= Seg (len H) by A65, A66, FINSEQ_1:def 3

.= Seg (len (Si . k)) by A64, INTEGR15:def 1

.= dom (Si . k) by FINSEQ_1:def 3 ;

A69: for j being Nat st j in dom (Im (S . k)) holds

(Im (S . k)) . j = (Si . k) . j

(Im (S . k)) . j0 = (Si . k) . j0 by A69;

thus rseqi . k = Im (xseq . k) by COMSEQ_3:def 6

.= Im (middle_sum (f,(S . k))) by Def4

.= middle_sum ((Im f),(Si . k)) by A78, A68, Th8, FUNCT_1:2

.= (middle_sum ((Im f),Si)) . k by INTEGR15:def 4 ; :: thesis: verum

end;consider H, z being FinSequence such that

A64: H = T . k and

A65: z = S . k and

A66: len H = len z and

A67: for j being Element of NAT st j in dom H holds

ex rji being Element of COMPLEX ex tji being Element of REAL st

( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A54;

A68: dom (Im (S . k)) = dom (S . k) by COMSEQ_3:def 4

.= Seg (len H) by A65, A66, FINSEQ_1:def 3

.= Seg (len (Si . k)) by A64, INTEGR15:def 1

.= dom (Si . k) by FINSEQ_1:def 3 ;

A69: for j being Nat st j in dom (Im (S . k)) holds

(Im (S . k)) . j = (Si . k) . j

proof

A78:
for j0 being object st j0 in dom (Im (S . k)) holds
let j0 be Nat; :: thesis: ( j0 in dom (Im (S . k)) implies (Im (S . k)) . j0 = (Si . k) . j0 )

reconsider j = j0 as Element of NAT by ORDINAL1:def 12;

assume A70: j0 in dom (Im (S . k)) ; :: thesis: (Im (S . k)) . j0 = (Si . k) . j0

then j0 in Seg (len (Si . k)) by A68, FINSEQ_1:def 3;

then j0 in Seg (len H) by A64, INTEGR15:def 1;

then j in dom H by FINSEQ_1:def 3;

then consider rji being Element of COMPLEX , tji being Element of REAL such that

A71: tji in dom (f | (divset ((T . k),j))) and

A72: (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) and

A73: rji = (f | (divset ((T . k),j))) . tji and

A74: z . j = (vol (divset ((T . k),j))) * rji by A67;

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

.= (dom (Im f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 4

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

then tji in (dom (Im f)) /\ (divset ((T . k),j)) by A71, RELAT_1:61;

then A76: tji in dom (Im f) by XBOOLE_0:def 4;

A77: ((Im f) | (divset ((T . k),j))) . tji = (Im f) . tji by A71, A75, FUNCT_1:47

.= Im (f . tji) by A76, COMSEQ_3:def 4

.= Im rji by A71, A73, FUNCT_1:47 ;

(Im (S . k)) . j = Im ((S . k) . j) by A70, COMSEQ_3:def 4

.= (Si . k) . j by A72, A77, A65, A74, Th1 ;

hence (Im (S . k)) . j0 = (Si . k) . j0 ; :: thesis: verum

end;reconsider j = j0 as Element of NAT by ORDINAL1:def 12;

assume A70: j0 in dom (Im (S . k)) ; :: thesis: (Im (S . k)) . j0 = (Si . k) . j0

then j0 in Seg (len (Si . k)) by A68, FINSEQ_1:def 3;

then j0 in Seg (len H) by A64, INTEGR15:def 1;

then j in dom H by FINSEQ_1:def 3;

then consider rji being Element of COMPLEX , tji being Element of REAL such that

A71: tji in dom (f | (divset ((T . k),j))) and

A72: (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) and

A73: rji = (f | (divset ((T . k),j))) . tji and

A74: z . j = (vol (divset ((T . k),j))) * rji by A67;

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

.= (dom (Im f)) /\ (divset ((T . k),j)) by COMSEQ_3:def 4

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

then tji in (dom (Im f)) /\ (divset ((T . k),j)) by A71, RELAT_1:61;

then A76: tji in dom (Im f) by XBOOLE_0:def 4;

A77: ((Im f) | (divset ((T . k),j))) . tji = (Im f) . tji by A71, A75, FUNCT_1:47

.= Im (f . tji) by A76, COMSEQ_3:def 4

.= Im rji by A71, A73, FUNCT_1:47 ;

(Im (S . k)) . j = Im ((S . k) . j) by A70, COMSEQ_3:def 4

.= (Si . k) . j by A72, A77, A65, A74, Th1 ;

hence (Im (S . k)) . j0 = (Si . k) . j0 ; :: thesis: verum

(Im (S . k)) . j0 = (Si . k) . j0 by A69;

thus rseqi . k = Im (xseq . k) by COMSEQ_3:def 6

.= Im (middle_sum (f,(S . k))) by Def4

.= middle_sum ((Im f),(Si . k)) by A78, A68, Th8, FUNCT_1:2

.= (middle_sum ((Im f),Si)) . k by INTEGR15:def 4 ; :: thesis: verum

then Im f is integrable by A42, INTEGR15:10;

hence f is integrable by A41; :: 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