let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,COMPLEX; :: thesis:
assume A1: f is bounded ; :: thesis:

hereby :: thesis:

reconsider I = integral f as Element of COMPLEX ;
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, Th14; :: thesis:

end;

now :: thesis:

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

set x = I;
let T be DivSequence of A; :: thesis:
let Si be middle_volume_Sequence of Re 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 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₁[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 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₂[j,x]

proof

let j0 be Nat; :: thesis:
assume A7: j0 in Seg (len Tk) ; :: thesis:
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:
thus S₂[j0,x] by A9, A10, A11, A12; :: thesis:

end;

consider p being FinSequence of COMPLEX such that
A13: ( 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(A6);
reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;
take x ; :: thesis:

A14: now :: thesis:

let jj0 be Element of NAT ; :: thesis:
reconsider j0 = jj0 as Nat ;
A15: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
assume jj0 in dom Tk ; :: thesis:
then S₂[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:

end;

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

end;

consider S being sequence of (COMPLEX *) such that
A16: for x being Element of NAT holds S₁[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

proof

let k be Element of NAT ; :: thesis:
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:

let x be Nat; :: thesis:
assume A20: x in dom H ; :: thesis:
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:
thus rji in rng (f | (divset ((T . k),x))) by A21, A22, FUNCT_1:3; :: thesis:
thus z . x = rji * (vol (divset ((T . k),x))) by A23; :: thesis:

end;

thus S . k is middle_volume of f,T . k by A17, A19, Def1; :: thesis:

end;

then reconsider S = S as middle_volume_Sequence of f,T by Def3;
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:
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

let k be Element of NAT ; :: thesis:
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

let j0 be Nat; :: thesis:
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
assume A32: j0 in dom (Re (S . k)) ; :: thesis:
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:

end;

A40: for j0 being object st j0 in dom (Re (S . k)) holds
(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:

end;

hence ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii ) by A25, FUNCT_2:63; :: thesis:

end;

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

A42: now :: thesis:

set x = I;
let T be DivSequence of A; :: thesis:
let Si be middle_volume_Sequence of Im 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 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₁[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 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₂[j,x]

proof

let j0 be Nat; :: thesis:
assume A45: j0 in Seg (len Tk) ; :: thesis:
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:
thus S₂[j0,x] by A47, A48, A49, A50; :: thesis:

end;

consider p being FinSequence of COMPLEX such that
A51: ( 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(A44);
reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;
take x ; :: thesis:

A52: now :: thesis:

let jj0 be Element of NAT ; :: thesis:
reconsider j0 = jj0 as Nat ;
A53: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
assume jj0 in dom Tk ; :: thesis:
then S₂[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:

end;

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

end;

consider S being sequence of (COMPLEX *) such that
A54: for x being Element of NAT holds S₁[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

proof

let k be Element of NAT ; :: thesis:
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:

let x be Nat; :: thesis:
assume A58: x in dom H ; :: thesis:
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:
thus rji in rng (f | (divset ((T . k),x))) by A59, A60, FUNCT_1:3; :: thesis:
thus z . x = rji * (vol (divset ((T . k),x))) by A61; :: thesis:

end;

thus S . k is middle_volume of f,T . k by A55, A57, Def1; :: thesis:

end;

then reconsider S = S as middle_volume_Sequence of f,T by Def3;
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:
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

let k be Element of NAT ; :: thesis:
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

let j0 be Nat; :: thesis:
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
assume A70: j0 in dom (Im (S . k)) ; :: thesis:
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:

end;

A78: for j0 being object st j0 in dom (Im (S . k)) holds
(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:

end;

hence ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) by A63, FUNCT_2:63; :: thesis:

end;

Im f is bounded by A1, Th13;
then Im f is integrable by A42, INTEGR15:10;
hence f is integrable by A41; :: thesis:

end;

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