let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,COMPLEX; :: thesis:
let T be DivSequence of A; :: thesis:
let S be middle_volume_Sequence of f,T; :: thesis:
assume that
A1: ( f is bounded & f is integrable ) and
A2: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
set seq = middle_sum (f,S);
set xs = integral f;
A3: ( Re f is bounded & Re f is integrable ) by A1, Th13;
A4: ( Im f is bounded & Im f is integrable ) by A1, Th13;
reconsider xseq = middle_sum (f,S) as sequence of COMPLEX ;
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi )

reconsider pjinf = Re f as Function of A,REAL ;
defpred S₁[ Element of NAT , set ] means $2 = Re (S . $1);
A5: for x being Element of NAT ex y being Element of REAL * st S₁[x,y]

end;

consider F being sequence of (REAL *) such that
A6: for x being Element of NAT holds S₁[x,F . x] from FUNCT_2:sch 3(A5);
A7: for x being Element of NAT holds dom (Re (S . x)) = Seg (len (S . x))

let x be Element of NAT ; :: thesis:
thus dom (Re (S . x)) = dom (S . x) by COMSEQ_3:def 3
.= Seg (len (S . x)) by FINSEQ_1:def 3 ; :: thesis:

end;

for k being Element of NAT holds F . k is middle_volume of pjinf,T . k

let k be Element of NAT ; :: thesis:
set Tk = T . k;
reconsider Fk = F . k as FinSequence of REAL ;
A8: F . k = Re (S . k) by A6;
then A9: dom Fk = Seg (len (S . k)) by A7
.= Seg (len (T . k)) by Def1 ;
then A10: dom Fk = dom (T . k) by FINSEQ_1:def 3;

let j be Nat; :: thesis:
assume A12: j in dom (T . k) ; :: thesis:
then consider r being Element of COMPLEX such that
A13: r in rng (f | (divset ((T . k),j))) and
A14: (S . k) . j = r * (vol (divset ((T . k),j))) by Def1;
reconsider v = Re r as Element of REAL ;
take v = v; :: thesis:
consider t being object such that
A15: t in dom (f | (divset ((T . k),j))) and
A16: r = (f | (divset ((T . k),j))) . t by A13, FUNCT_1:def 3;
t in (dom f) /\ (divset ((T . k),j)) by A15, RELAT_1:61;
then t in dom f by XBOOLE_0:def 4;
then A17: t in dom (Re f) by COMSEQ_3:def 3;
A18: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom pjinf) /\ (divset ((T . k),j)) by COMSEQ_3:def 3
.= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ;
Re r = Re (f . t) by A15, A16, FUNCT_1:47
.= (Re f) . t by A17, COMSEQ_3:def 3
.= (pjinf | (divset ((T . k),j))) . t by A15, A18, FUNCT_1:47 ;
hence v in rng (pjinf | (divset ((T . k),j))) by A15, A18, FUNCT_1:3; :: thesis:
thus Fk . j = Re ((S . k) . j) by A8, A10, A12, COMSEQ_3:def 3
.= v * (vol (divset ((T . k),j))) by A14, Th1 ; :: thesis:

end;

end;

then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
reconsider rseqi = middle_sum (pjinf,pjis) as Real_Sequence ;
A19: for k being Nat holds rseqi . k = Re (xseq . k)

let k be Nat; :: thesis:
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
A20: Re (S . kk) is middle_volume of Re f,T . kk by Th4;
thus rseqi . k = middle_sum (pjinf,(pjis . kk)) by INTEGR15:def 4
.= Re (middle_sum (f,(S . kk))) by A6, A20, Th7
.= Re (xseq . k) by Def4 ; :: thesis:

end;

take rseqi ; :: thesis:
lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, A3, INTEGR15:9;
hence for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) by A2, A3, A19, COMPLEX1:12, INTEGR15:9; :: thesis:

end;

then consider rseqi being Real_Sequence such that
A21: for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) ;
ex iseqi being Real_Sequence st
for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi )

reconsider pjinf = Im f as Function of A,REAL ;
defpred S₁[ Element of NAT , set ] means $2 = Im (S . $1);
A22: for x being Element of NAT ex y being Element of REAL * st S₁[x,y]

end;

consider F being sequence of (REAL *) such that
A23: for x being Element of NAT holds S₁[x,F . x] from FUNCT_2:sch 3(A22);
A24: for x being Element of NAT holds dom (Im (S . x)) = Seg (len (S . x))

let x be Element of NAT ; :: thesis:
dom (Im (S . x)) = dom (S . x) by COMSEQ_3:def 4
.= Seg (len (S . x)) by FINSEQ_1:def 3 ;
hence dom (Im (S . x)) = Seg (len (S . x)) ; :: thesis:

end;

for k being Element of NAT holds F . k is middle_volume of pjinf,T . k

let k be Element of NAT ; :: thesis:
reconsider Tk = T . k as FinSequence ;
reconsider Fk = F . k as FinSequence of REAL ;
A25: F . k = Im (S . k) by A23;
then A26: dom Fk = Seg (len (S . k)) by A24
.= Seg (len Tk) by Def1 ;
then A27: dom Fk = dom Tk by FINSEQ_1:def 3;

let j be Nat; :: thesis:
assume A29: j in dom Tk ; :: thesis:
then consider r being Element of COMPLEX such that
A30: r in rng (f | (divset ((T . k),j))) and
A31: (S . k) . j = r * (vol (divset ((T . k),j))) by Def1;
reconsider v = Im r as Element of REAL ;
take v = v; :: thesis:
consider t being object such that
A32: t in dom (f | (divset ((T . k),j))) and
A33: r = (f | (divset ((T . k),j))) . t by A30, FUNCT_1:def 3;
t in (dom f) /\ (divset ((T . k),j)) by A32, RELAT_1:61;
then t in dom f by XBOOLE_0:def 4;
then A34: t in dom (Im f) by COMSEQ_3:def 4;
A35: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom pjinf) /\ (divset ((T . k),j)) by COMSEQ_3:def 4
.= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ;
Im r = Im (f . t) by A32, A33, FUNCT_1:47
.= (Im f) . t by A34, COMSEQ_3:def 4
.= (pjinf | (divset ((T . k),j))) . t by A32, A35, FUNCT_1:47 ;
hence v in rng (pjinf | (divset ((T . k),j))) by A32, A35, FUNCT_1:3; :: thesis:
thus Fk . j = Im ((S . k) . j) by A25, A27, A29, COMSEQ_3:def 4
.= v * (vol (divset ((T . k),j))) by A31, Th1 ; :: thesis:

end;

end;

then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
reconsider iseqi = middle_sum (pjinf,pjis) as Real_Sequence ;
A36: for k being Nat holds iseqi . k = Im (xseq . k)

let k be Nat; :: thesis:
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
A37: Im (S . kk) is middle_volume of Im f,T . kk by Th4;
thus iseqi . k = middle_sum (pjinf,(pjis . kk)) by INTEGR15:def 4
.= Im (middle_sum (f,(S . kk))) by A23, A37, Th8
.= Im (xseq . k) by Def4 ; :: thesis:

end;

take iseqi ; :: thesis:
lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, A4, INTEGR15:9;
hence for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) by A2, A4, A36, COMPLEX1:12, INTEGR15:9; :: thesis:

end;

then consider iseqi being Real_Sequence such that
A38: for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) ;
thus middle_sum (f,S) is convergent by A21, A38, COMSEQ_3:38; :: thesis:
thus lim (middle_sum (f,S)) = (lim rseqi) + ((lim iseqi) * <i>) by A21, A38, COMSEQ_3:39
.= integral f by A21, A38, COMPLEX1:13 ; :: thesis: