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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 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 )

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 )

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: lim (middle_sum (f,S)) = integral f

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

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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 (delta T) = 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 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 )

proof

then consider rseqi being Real_Sequence such that
reconsider pjinf = Re f as Function of A,REAL ;

defpred S_{1}[ Element of NAT , set ] means $2 = Re (S . $1);

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

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

reconsider rseqi = middle_sum (pjinf,pjis) as Real_Sequence ;

A19: for k being Nat holds rseqi . k = Re (xseq . k)

( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi )

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

end;defpred S

A5: for x being Element of NAT ex y being Element of REAL * st S

proof

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

Re (S . x) is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S_{1}[x,y]
; :: thesis: verum

end;Re (S . x) is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S

A6: for x being Element of NAT holds S

A7: for x being Element of NAT holds dom (Re (S . x)) = Seg (len (S . x))

proof

for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
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;thus dom (Re (S . x)) = dom (S . x) by COMSEQ_3:def 3

.= Seg (len (S . x)) by FINSEQ_1:def 3 ; :: thesis: verum

proof

then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
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;

hence F . k is middle_volume of pjinf,T . k by A11, INTEGR15:def 1; :: thesis: verum

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

len Fk = len (T . k)
by A9, FINSEQ_1:def 3;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 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: Fk . j = v * (vol (divset ((T . k),j)))

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

end;( 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 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: Fk . j = v * (vol (divset ((T . k),j)))

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

hence F . k is middle_volume of pjinf,T . k by A11, INTEGR15:def 1; :: thesis: verum

reconsider rseqi = middle_sum (pjinf,pjis) as Real_Sequence ;

A19: for k being Nat holds rseqi . k = Re (xseq . k)

proof

take
rseqi
; :: thesis: for k being Nat holds
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;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

( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi )

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

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 )

proof

then consider iseqi being Real_Sequence such that
reconsider pjinf = Im f as Function of A,REAL ;

defpred S_{1}[ Element of NAT , set ] means $2 = Im (S . $1);

A22: for x being Element of NAT ex y being Element of REAL * st S_{1}[x,y]

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

reconsider iseqi = middle_sum (pjinf,pjis) as Real_Sequence ;

A36: for k being Nat holds iseqi . k = Im (xseq . k)

( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi )

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

end;defpred S

A22: for x being Element of NAT ex y being Element of REAL * st S

proof

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

Im (S . x) is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S_{1}[x,y]
; :: thesis: verum

end;Im (S . x) is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S

A23: for x being Element of NAT holds S

A24: for x being Element of NAT holds dom (Im (S . x)) = Seg (len (S . x))

proof

for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
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;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

proof

then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
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;

hence F . k is middle_volume of pjinf,T . k by A28, INTEGR15:def 1; :: thesis: verum

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

len Fk = len Tk
by A26, FINSEQ_1:def 3;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 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: Fk . j = v * (vol (divset ((T . k),j)))

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

end;( 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 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: Fk . j = v * (vol (divset ((T . k),j)))

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

hence F . k is middle_volume of pjinf,T . k by A28, INTEGR15:def 1; :: thesis: verum

reconsider iseqi = middle_sum (pjinf,pjis) as Real_Sequence ;

A36: for k being Nat holds iseqi . k = Im (xseq . k)

proof

take
iseqi
; :: thesis: for k being Nat holds
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 A23, A37, Th8

.= Im (xseq . k) by Def4 ; :: thesis: verum

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

( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi )

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

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: lim (middle_sum (f,S)) = integral f

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