let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,COMPLEX
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

let f be Function of A,COMPLEX; :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

let S be middle_volume_Sequence of f,T; :: thesis: ( f is bounded & f is integrable & delta T is convergent & lim () = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) )
assume that
A1: ( f is bounded & f is integrable ) and
A2: ( delta T is convergent & lim () = 0 ) ; :: thesis: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
set seq = middle_sum (f,S);
set xs = integral f;
A3: ( Re f is bounded & Re f is integrable ) by ;
A4: ( Im f is bounded & Im f is integrable ) by ;
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 () = lim rseqi )
proof
reconsider pjinf = Re f as Function of A,REAL ;
defpred S1[ Element of NAT , set ] means \$2 = Re (S . \$1);
A5: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S1[x,y]
Re (S . x) is Element of REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S1[x,y] ; :: thesis: verum
end;
consider F being sequence of () such that
A6: for x being Element of NAT holds S1[x,F . x] from A7: for x being Element of NAT holds dom (Re (S . x)) = Seg (len (S . x))
proof
let x be Element of NAT ; :: thesis: dom (Re (S . x)) = Seg (len (S . x))
thus dom (Re (S . x)) = dom (S . x) by COMSEQ_3:def 3
.= Seg (len (S . x)) by FINSEQ_1:def 3 ; :: thesis: verum
end;
for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
proof
let k be Element of NAT ; :: thesis: F . k is middle_volume of pjinf,T . k
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;
A11: now :: thesis: for j being Nat st j in dom (T . k) holds
ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
let j be Nat; :: thesis: ( j in dom (T . k) implies ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) )

assume A12: j in dom (T . k) ; :: thesis: ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )

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: ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
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 ;
t in (dom f) /\ (divset ((T . k),j)) by ;
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
.= (Re f) . t by
.= (pjinf | (divset ((T . k),j))) . t by ;
hence v in rng (pjinf | (divset ((T . k),j))) by ; :: thesis: Fk . j = v * (vol (divset ((T . k),j)))
thus Fk . j = Re ((S . k) . j) by
.= v * (vol (divset ((T . k),j))) by ; :: thesis: verum
end;
len Fk = len (T . k) by ;
hence F . k is middle_volume of pjinf,T . k by ; :: thesis: verum
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)
proof
let k be Nat; :: thesis: rseqi . k = Re (xseq . k)
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: verum
end;
take rseqi ; :: thesis: for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re () = lim rseqi )

lim (middle_sum (pjinf,pjis)) = integral pjinf by ;
hence for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re () = lim rseqi ) by ; :: thesis: verum
end;
then consider rseqi being Real_Sequence such that
A21: for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re () = lim rseqi ) ;
ex iseqi being Real_Sequence st
for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im () = lim iseqi )
proof
reconsider pjinf = Im f as Function of A,REAL ;
defpred S1[ Element of NAT , set ] means \$2 = Im (S . \$1);
A22: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S1[x,y]
Im (S . x) is Element of REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S1[x,y] ; :: thesis: verum
end;
consider F being sequence of () such that
A23: for x being Element of NAT holds S1[x,F . x] from A24: for x being Element of NAT holds dom (Im (S . x)) = Seg (len (S . x))
proof
let x be Element of NAT ; :: thesis: dom (Im (S . x)) = Seg (len (S . x))
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: verum
end;
for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
proof
let k be Element of NAT ; :: thesis: F . k is middle_volume of pjinf,T . k
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;
A28: now :: thesis: for j being Nat st j in dom Tk holds
ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
let j be Nat; :: thesis: ( j in dom Tk implies ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) )

assume A29: j in dom Tk ; :: thesis: ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )

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: ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
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 ;
t in (dom f) /\ (divset ((T . k),j)) by ;
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
.= (Im f) . t by
.= (pjinf | (divset ((T . k),j))) . t by ;
hence v in rng (pjinf | (divset ((T . k),j))) by ; :: thesis: Fk . j = v * (vol (divset ((T . k),j)))
thus Fk . j = Im ((S . k) . j) by
.= v * (vol (divset ((T . k),j))) by ; :: thesis: verum
end;
len Fk = len Tk by ;
hence F . k is middle_volume of pjinf,T . k by ; :: thesis: verum
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)
proof
let k be Nat; :: thesis: iseqi . k = Im (xseq . k)
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
.= Im (xseq . k) by Def4 ; :: thesis: verum
end;
take iseqi ; :: thesis: for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im () = lim iseqi )

lim (middle_sum (pjinf,pjis)) = integral pjinf by ;
hence for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im () = lim iseqi ) by ; :: thesis: verum
end;
then consider iseqi being Real_Sequence such that
A38: for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im () = lim iseqi ) ;
thus middle_sum (f,S) is convergent by ; :: thesis: lim (middle_sum (f,S)) = integral f
thus lim (middle_sum (f,S)) = (lim rseqi) + ((lim iseqi) * <i>) by
.= integral f by ; :: thesis: verum