let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,COMPLEX st f is bounded holds
( f is integrable iff 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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

let f be Function of A,COMPLEX; :: thesis: ( f is bounded implies ( f is integrable iff 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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) )

assume A1: f is bounded ; :: thesis: ( f is integrable iff 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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

hereby :: thesis: ( 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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )
reconsider I = integral f as Element of COMPLEX ;
assume A2: f is integrable ; :: thesis: 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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )

take I = I; :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )

thus for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th14; :: thesis: verum
end;
now :: thesis: ( 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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )
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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; :: thesis: f is integrable
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 () = 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: for T being DivSequence of A
for Si being middle_volume_Sequence of Re f,T st delta T is convergent & lim () = 0 holds
( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )
set x = I;
let T be DivSequence of A; :: thesis: for Si being middle_volume_Sequence of Re f,T st delta T is convergent & lim () = 0 holds
( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )

let Si be middle_volume_Sequence of Re f,T; :: thesis: ( delta T is convergent & lim () = 0 implies ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii ) )
defpred S1[ 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 S1[k,y]
proof
let k be Element of NAT ; :: thesis: ex y being Element of COMPLEX * st S1[k,y]
reconsider Tk = T . k as FinSequence ;
defpred S2[ 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 S2[j,x]
proof
let j0 be Nat; :: thesis: ( j0 in Seg (len Tk) implies ex x being Element of COMPLEX st S2[j0,x] )
assume A7: j0 in Seg (len Tk) ; :: thesis: ex x being Element of COMPLEX st S2[j0,x]
then reconsider j = j0 as Element of NAT ;
j in dom Tk by ;
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 ;
tji in (dom (Re f)) /\ (divset ((T . k),j)) by ;
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 ;
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: S2[j0,x]
thus S2[j0,x] by A9, A10, A11, A12; :: thesis: verum
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
S2[j,p . j] ) ) from reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;
take x ; :: thesis: S1[k,x]
A14: now :: thesis: for jj0 being Element of NAT st jj0 in dom Tk holds
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 )
let jj0 be Element of NAT ; :: thesis: ( jj0 in dom Tk implies 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 ) )

reconsider j0 = jj0 as Nat ;
A15: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
assume jj0 in dom Tk ; :: thesis: 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 )

then S2[j0,p . j0] by ;
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: verum
end;
len p = len Tk by ;
hence S1[k,x] by A14; :: thesis: verum
end;
consider S being sequence of () such that
A16: for x being Element of NAT holds S1[x,S . x] from for k being Element of NAT holds S . k is middle_volume of f,T . k
proof
let k be Element of NAT ; :: thesis: S . k is middle_volume of f,T . k
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: for x being Nat st x in dom H holds
ex rji being Element of COMPLEX st
( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) )
let x be Nat; :: thesis: ( x in dom H implies ex rji being Element of COMPLEX st
( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) )

assume A20: x in dom H ; :: thesis: ex rji being Element of COMPLEX st
( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) )

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 ;
take rji = rji; :: thesis: ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) )
thus rji in rng (f | (divset ((T . k),x))) by ; :: thesis: z . x = rji * (vol (divset ((T . k),x)))
thus z . x = rji * (vol (divset ((T . k),x))) by A23; :: thesis: verum
end;
thus S . k is middle_volume of f,T . k by ; :: thesis: verum
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 () = 0 ) ; :: thesis: ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii )
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 ;
for k being Element of NAT holds rseqi . k = (middle_sum ((Re f),Si)) . k
proof
let k be Element of NAT ; :: thesis: rseqi . k = (middle_sum ((Re f),Si)) . k
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
.= Seg (len (Si . k)) by
.= 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: ( j0 in dom (Re (S . k)) implies (Re (S . k)) . j0 = (Si . k) . j0 )
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
assume A32: j0 in dom (Re (S . k)) ; :: thesis: (Re (S . k)) . j0 = (Si . k) . j0
then j0 in Seg (len (Si . k)) by ;
then j0 in Seg (len H) by ;
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 ;
then A38: tji in dom (Re f) by XBOOLE_0:def 4;
A39: ((Re f) | (divset ((T . k),j))) . tji = (Re f) . tji by
.= Re (f . tji) by
.= Re rji by ;
(Re (S . k)) . j = Re ((S . k) . j) by
.= (Si . k) . j by A34, A39, Th1, A27, A36 ;
hence (Re (S . k)) . j0 = (Si . k) . j0 ; :: thesis: verum
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
.= (middle_sum ((Re f),Si)) . k by INTEGR15:def 4 ; :: thesis: verum
end;
hence ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii ) by ; :: thesis: verum
end;
Re f is bounded by ;
then A41: Re f is integrable by ;
A42: now :: thesis: for T being DivSequence of A
for Si being middle_volume_Sequence of Im f,T st delta T is convergent & lim () = 0 holds
( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )
set x = I;
let T be DivSequence of A; :: thesis: for Si being middle_volume_Sequence of Im f,T st delta T is convergent & lim () = 0 holds
( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )

let Si be middle_volume_Sequence of Im f,T; :: thesis: ( delta T is convergent & lim () = 0 implies ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) )
defpred S1[ 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 S1[k,y]
proof
let k be Element of NAT ; :: thesis: ex y being Element of COMPLEX * st S1[k,y]
reconsider Tk = T . k as FinSequence ;
defpred S2[ 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 S2[j,x]
proof
let j0 be Nat; :: thesis: ( j0 in Seg (len Tk) implies ex x being Element of COMPLEX st S2[j0,x] )
assume A45: j0 in Seg (len Tk) ; :: thesis: ex x being Element of COMPLEX st S2[j0,x]
then reconsider j = j0 as Element of NAT ;
j in dom Tk by ;
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 ;
tji in (dom (Im f)) /\ (divset ((T . k),j)) by ;
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 ;
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: S2[j0,x]
thus S2[j0,x] by A47, A48, A49, A50; :: thesis: verum
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
S2[j,p . j] ) ) from reconsider x = p as Element of COMPLEX * by FINSEQ_1:def 11;
take x ; :: thesis: S1[k,x]
A52: now :: thesis: for jj0 being Element of NAT st jj0 in dom Tk holds
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 )
let jj0 be Element of NAT ; :: thesis: ( jj0 in dom Tk implies 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 ) )

reconsider j0 = jj0 as Nat ;
A53: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
assume jj0 in dom Tk ; :: thesis: 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 )

then S2[j0,p . j0] by ;
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: verum
end;
len p = len Tk by ;
hence S1[k,x] by A52; :: thesis: verum
end;
consider S being sequence of () such that
A54: for x being Element of NAT holds S1[x,S . x] from for k being Element of NAT holds S . k is middle_volume of f,T . k
proof
let k be Element of NAT ; :: thesis: S . k is middle_volume of f,T . k
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: for x being Nat st x in dom H holds
ex rji being Element of COMPLEX st
( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) )
let x be Nat; :: thesis: ( x in dom H implies ex rji being Element of COMPLEX st
( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) )

assume A58: x in dom H ; :: thesis: ex rji being Element of COMPLEX st
( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) )

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 ;
take rji = rji; :: thesis: ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) )
thus rji in rng (f | (divset ((T . k),x))) by ; :: thesis: z . x = rji * (vol (divset ((T . k),x)))
thus z . x = rji * (vol (divset ((T . k),x))) by A61; :: thesis: verum
end;
thus S . k is middle_volume of f,T . k by ; :: thesis: verum
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 () = 0 ) ; :: thesis: ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic )
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 ;
for k being Element of NAT holds rseqi . k = (middle_sum ((Im f),Si)) . k
proof
let k be Element of NAT ; :: thesis: rseqi . k = (middle_sum ((Im f),Si)) . k
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
.= Seg (len (Si . k)) by
.= 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: ( j0 in dom (Im (S . k)) implies (Im (S . k)) . j0 = (Si . k) . j0 )
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
assume A70: j0 in dom (Im (S . k)) ; :: thesis: (Im (S . k)) . j0 = (Si . k) . j0
then j0 in Seg (len (Si . k)) by ;
then j0 in Seg (len H) by ;
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 ;
then A76: tji in dom (Im f) by XBOOLE_0:def 4;
A77: ((Im f) | (divset ((T . k),j))) . tji = (Im f) . tji by
.= Im (f . tji) by
.= Im rji by ;
(Im (S . k)) . j = Im ((S . k) . j) by
.= (Si . k) . j by A72, A77, A65, A74, Th1 ;
hence (Im (S . k)) . j0 = (Si . k) . j0 ; :: thesis: verum
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
.= (middle_sum ((Im f),Si)) . k by INTEGR15:def 4 ; :: thesis: verum
end;
hence ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) by ; :: thesis: verum
end;
Im f is bounded by ;
then Im f is integrable by ;
hence f is integrable by A41; :: thesis: verum
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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; :: thesis: verum