let A be 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, Th11; :: thesis:

end;

now

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

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 ;
reconsider Sik = Si . k as FinSequence of REAL ;
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 A60: j0 in Seg (len Tk) ; :: thesis:
then reconsider j = j0 as Element of NAT ;
j in dom Tk by A60, FINSEQ_1:def 3;
then consider r being Element of REAL such that
A61: r in rng ((Re f) | (divset (T . k),j)) and
A62: (Si . k) . j = r * (vol (divset (T . k),j)) by INTEGR15:def 1;
consider tji being set such that
A63: tji in dom ((Re f) | (divset (T . k),j)) and
A64: r = ((Re f) | (divset (T . k),j)) . tji by A61, FUNCT_1:def 5;
tji in (dom (Re f)) /\ (divset (T . k),j) by A63, RELAT_1:90;
then reconsider tji = tji as Element of REAL ;
A65: dom (f | (divset (T . k),j)) = (dom f) /\ (divset (T . k),j) by RELAT_1:90
.= (dom (Re f)) /\ (divset (T . k),j) by COMSEQ_3:def 3
.= dom ((Re f) | (divset (T . k),j)) by RELAT_1:90 ;
then (f | (divset (T . k),j)) . tji in rng (f | (divset (T . k),j)) by A63, FUNCT_1:12;
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 ;
take x ; :: thesis:
thus S₂[j0,x] by A62, A63, A64, A65; :: thesis:

end;

consider p being FinSequence of COMPLEX such that
A7: ( 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:

A8: now

let jj0 be Element of NAT ; :: thesis:
reconsider j0 = jj0 as Nat ;
A81: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
assume jj0 in dom Tk ; :: thesis:
then S₂[j0,p . j0] by A7, A81;
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 A7, FINSEQ_1:def 3;
hence S₁[k,x] by A8; :: thesis:

end;

consider S being Function of NAT ,(COMPLEX * ) such that
A9: for x being Element of NAT holds S₁[x,S . x] from FUNCT_2:sch 10(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
A10: ( H = T . k & z = S . k & len H = len z ) and
A11: 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 A9;

A12: now

let x be Nat; :: thesis:
assume A120: 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
A121: 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
A122: rji = (f | (divset (T . k),j)) . tji and
A123: z . j = (vol (divset (T . k),j)) * rji by A11, A120;
take rji = rji; :: thesis:
thus rji in rng (f | (divset (T . k),x)) by A121, A122, FUNCT_1:12; :: thesis:
thus z . x = rji * (vol (divset (T . k),x)) by A123; :: thesis:

end;

S . k is FinSequence of COMPLEX by FINSEQ_1:def 11;
hence S . k is middle_volume of f,T . k by A10, A12, Def5; :: thesis:

end;

then reconsider S = S as middle_volume_Sequence of f,T by Def7;
set seq = middle_sum f,S;
reconsider xseq = middle_sum f,S as Function of NAT ,COMPLEX ;
assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
then U1: ( middle_sum f,S is convergent & lim (middle_sum f,S) = I ) by A3;
reconsider rseqi = Re (middle_sum f,S) as Real_Sequence ;
A20: for k being Element of NAT holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re xs = lim rseqi ) by U1, 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
A21: H = T . k and
A22: z = S . k and
A23: len H = len z and
A24: 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 A9;
A25: dom (Re (S . k)) = dom (S . k) by COMSEQ_3:def 3
.= Seg (len H) by A22, A23, FINSEQ_1:def 3
.= Seg (len (Si . k)) by A21, INTEGR15:def 1
.= dom (Si . k) by FINSEQ_1:def 3 ;
A26: 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 13;
assume A260: j0 in dom (Re (S . k)) ; :: thesis:
then j0 in Seg (len (Si . k)) by A25, FINSEQ_1:def 3;
then j0 in Seg (len H) by A21, 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
A261: tji in dom (f | (divset (T . k),j)) and
A262: (Si . k) . j = (vol (divset (T . k),j)) * (((Re f) | (divset (T . k),j)) . tji) and
A263: rji = (f | (divset (T . k),j)) . tji and
A264: z . j = (vol (divset (T . k),j)) * rji by A24;
A265: dom (f | (divset (T . k),j)) = (dom f) /\ (divset (T . k),j) by RELAT_1:90
.= (dom (Re f)) /\ (divset (T . k),j) by COMSEQ_3:def 3
.= dom ((Re f) | (divset (T . k),j)) by RELAT_1:90 ;
then tji in (dom (Re f)) /\ (divset (T . k),j) by A261, RELAT_1:90;
then A266: tji in dom (Re f) by XBOOLE_0:def 4;
A267: ((Re f) | (divset (T . k),j)) . tji = (Re f) . tji by A261, A265, FUNCT_1:70
.= Re (f . tji) by A266, COMSEQ_3:def 3
.= Re rji by A261, A263, FUNCT_1:70 ;
(Re (S . k)) . j = Re ((S . k) . j) by A260, COMSEQ_3:def 3
.= (Si . k) . j by A262, A267, LM001, A22, A264 ;
hence (Re (S . k)) . j0 = (Si . k) . j0 ; :: thesis:

end;

reconsider Fi = Re (S . k) as middle_volume of Re f,T . k by LMDef5;
A27: for j0 being set st j0 in dom (Re (S . k)) holds
(Re (S . k)) . j0 = (Si . k) . j0 by A26;
thus rseqi . k = Re (xseq . k) by COMSEQ_3:def 5
.= Re (middle_sum f,(S . k)) by Def8
.= middle_sum (Re f),(Si . k) by A25, A27, FUNCT_1:9, LMDefR0
.= (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 A20, FUNCT_2:113; :: thesis:

end;

Re f is bounded by A1, BND01;
then X1: Re f is integrable by A4, INTEGR15:10;

B1: now

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 ;
B2: 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 ;
reconsider Sik = Si . k as FinSequence of REAL ;
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 ) );
B3: 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 B30: j0 in Seg (len Tk) ; :: thesis:
then reconsider j = j0 as Element of NAT ;
j in dom Tk by B30, FINSEQ_1:def 3;
then consider r being Element of REAL such that
B31: r in rng ((Im f) | (divset (T . k),j)) and
B32: (Si . k) . j = r * (vol (divset (T . k),j)) by INTEGR15:def 1;
consider tji being set such that
B33: tji in dom ((Im f) | (divset (T . k),j)) and
B34: r = ((Im f) | (divset (T . k),j)) . tji by B31, FUNCT_1:def 5;
tji in (dom (Im f)) /\ (divset (T . k),j) by B33, RELAT_1:90;
then reconsider tji = tji as Element of REAL ;
B35: dom (f | (divset (T . k),j)) = (dom f) /\ (divset (T . k),j) by RELAT_1:90
.= (dom (Im f)) /\ (divset (T . k),j) by COMSEQ_3:def 4
.= dom ((Im f) | (divset (T . k),j)) by RELAT_1:90 ;
then (f | (divset (T . k),j)) . tji in rng (f | (divset (T . k),j)) by B33, FUNCT_1:12;
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 ;
take x ; :: thesis:
thus S₂[j0,x] by B32, B33, B34, B35; :: thesis:

end;

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

B5: now

let jj0 be Element of NAT ; :: thesis:
reconsider j0 = jj0 as Nat ;
B51: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
assume jj0 in dom Tk ; :: thesis:
then S₂[j0,p . j0] by B4, B51;
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 B4, FINSEQ_1:def 3;
hence S₁[k,x] by B5; :: thesis:

end;

consider S being Function of NAT ,(COMPLEX * ) such that
B6: for x being Element of NAT holds S₁[x,S . x] from FUNCT_2:sch 10(B2);
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
B71: ( H = T . k & z = S . k & len H = len z ) and
B72: 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 B6;

B73: now

let x be Nat; :: thesis:
assume B74: 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
B75: 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
B76: rji = (f | (divset (T . k),j)) . tji and
B77: z . j = (vol (divset (T . k),j)) * rji by B72, B74;
take rji = rji; :: thesis:
thus rji in rng (f | (divset (T . k),x)) by B75, B76, FUNCT_1:12; :: thesis:
thus z . x = rji * (vol (divset (T . k),x)) by B77; :: thesis:

end;

S . k is FinSequence of COMPLEX by FINSEQ_1:def 11;
hence S . k is middle_volume of f,T . k by B71, B73, Def5; :: thesis:

end;

then reconsider S = S as middle_volume_Sequence of f,T by Def7;
set seq = middle_sum f,S;
reconsider xseq = middle_sum f,S as Function of NAT ,COMPLEX ;
assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
then U1: ( middle_sum f,S is convergent & lim (middle_sum f,S) = I ) by A3;
reconsider rseqi = Im (middle_sum f,S) as Real_Sequence ;
B8: for k being Element of NAT holds
( rseqi . k = Im (xseq . k) & rseqi is convergent & Im xs = lim rseqi ) by U1, 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
B90: H = T . k and
B91: z = S . k and
B92: len H = len z and
B93: 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 B6;
B94: dom (Im (S . k)) = dom (S . k) by COMSEQ_3:def 4
.= Seg (len H) by B91, B92, FINSEQ_1:def 3
.= Seg (len (Si . k)) by B90, INTEGR15:def 1
.= dom (Si . k) by FINSEQ_1:def 3 ;
B95: 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 13;
assume B950: j0 in dom (Im (S . k)) ; :: thesis:
then j0 in Seg (len (Si . k)) by B94, FINSEQ_1:def 3;
then j0 in Seg (len H) by B90, 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
B951: tji in dom (f | (divset (T . k),j)) and
B952: (Si . k) . j = (vol (divset (T . k),j)) * (((Im f) | (divset (T . k),j)) . tji) and
B953: rji = (f | (divset (T . k),j)) . tji and
B954: z . j = (vol (divset (T . k),j)) * rji by B93;
B955: dom (f | (divset (T . k),j)) = (dom f) /\ (divset (T . k),j) by RELAT_1:90
.= (dom (Im f)) /\ (divset (T . k),j) by COMSEQ_3:def 4
.= dom ((Im f) | (divset (T . k),j)) by RELAT_1:90 ;
then tji in (dom (Im f)) /\ (divset (T . k),j) by B951, RELAT_1:90;
then B956: tji in dom (Im f) by XBOOLE_0:def 4;
B957: ((Im f) | (divset (T . k),j)) . tji = (Im f) . tji by B951, B955, FUNCT_1:70
.= Im (f . tji) by B956, COMSEQ_3:def 4
.= Im rji by B951, B953, FUNCT_1:70 ;
(Im (S . k)) . j = Im ((S . k) . j) by B950, COMSEQ_3:def 4
.= (Si . k) . j by B952, B957, B91, B954, LM001 ;
hence (Im (S . k)) . j0 = (Si . k) . j0 ; :: thesis:

end;

reconsider Fi = Im (S . k) as middle_volume of Im f,T . k by LMDef5;
B96: for j0 being set st j0 in dom (Im (S . k)) holds
(Im (S . k)) . j0 = (Si . k) . j0 by B95;
thus rseqi . k = Im (xseq . k) by COMSEQ_3:def 6
.= Im (middle_sum f,(S . k)) by Def8
.= middle_sum (Im f),(Si . k) by B96, B94, FUNCT_1:9, LMDefI0
.= (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 B8, FUNCT_2:113; :: thesis:

end;

Im f is bounded by A1, BND01;
then Im f is integrable by B1, INTEGR15:10;
hence f is integrable by X1, Def13; :: 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: