let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL st f is bounded holds
( f is integrable iff ex I being Real 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 ) )
let f be Function of A,REAL ; :: thesis: ( f is bounded implies ( f is integrable iff ex I being Real 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 ) ) )
assume AS0: f is bounded ; :: thesis: ( f is integrable iff ex I being Real 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 ) )
dom f = A by FUNCT_2:def 1;
then AS: f | A is bounded by RELAT_1:98, AS0;

hereby :: thesis: ( ex I being Real 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 )

assume AS1: f is integrable ; :: thesis: ex I being Element of REAL 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 )
take I = integral f; :: thesis: 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 )
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 PX04, AS0, AS1; :: thesis: verum

end;

now

assume ex I being Real 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: f is integrable
then consider I being Real such that
AS2: 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 ) ;
X1: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
I = lim (lower_sum f,T)

proof

let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies I = lim (lower_sum f,T) )
assume AS3: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: I = lim (lower_sum f,T)
P1: ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f ) by AS, AS3, INTEGRA4:8;
consider S being middle_volume_Sequence of f,T;

P2: now

let i be Element of NAT ; :: thesis: 0 <= ((middle_sum f,S) - (lower_sum f,T)) . i
(lower_sum f,T) . i <= (middle_sum f,S) . i by PX011, AS;
then ((lower_sum f,T) . i) - ((lower_sum f,T) . i) <= ((middle_sum f,S) . i) - ((lower_sum f,T) . i) by XREAL_1:11;
hence 0 <= ((middle_sum f,S) - (lower_sum f,T)) . i by VALUED_1:15; :: thesis: verum

end;

P3: middle_sum f,S is convergent by AS2, AS3;
then P4: (middle_sum f,S) - (lower_sum f,T) is convergent by P1, SEQ_2:25;
lim ((middle_sum f,S) - (lower_sum f,T)) = (lim (middle_sum f,S)) - (lim (lower_sum f,T)) by P1, P3, SEQ_2:26
.= I - (lim (lower_sum f,T)) by AS2, AS3 ;
then X10: 0 <= I - (lim (lower_sum f,T)) by SEQ_2:31, P2, P4;

now

let e1 be real number ; :: thesis: ( 0 < e1 implies I - (lim (lower_sum f,T)) <= e1 )
assume A31: 0 < e1 ; :: thesis: I - (lim (lower_sum f,T)) <= e1
reconsider e = e1 as Real by XREAL_0:def 1;
consider S being middle_volume_Sequence of f,T such that
N1: for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e by A31, PX02, AS;

N2: now

let i be Element of NAT ; :: thesis: ((middle_sum f,S) - (lower_sum f,T)) . i <= e
(middle_sum f,S) . i <= ((lower_sum f,T) . i) + e by N1;
then ((middle_sum f,S) . i) - ((lower_sum f,T) . i) <= (((lower_sum f,T) . i) + e) - ((lower_sum f,T) . i) by XREAL_1:11;
hence ((middle_sum f,S) - (lower_sum f,T)) . i <= e by VALUED_1:15; :: thesis: verum

end;

N3: middle_sum f,S is convergent by AS2, AS3;
then N4: (middle_sum f,S) - (lower_sum f,T) is convergent by P1, SEQ_2:25;
lim ((middle_sum f,S) - (lower_sum f,T)) = (lim (middle_sum f,S)) - (lim (lower_sum f,T)) by P1, N3, SEQ_2:26
.= I - (lim (lower_sum f,T)) by AS2, AS3 ;
hence I - (lim (lower_sum f,T)) <= e1 by N2, N4, PREPOWER:3; :: thesis: verum

end;

then I - (lim (lower_sum f,T)) = 0 by XREAL_1:7, X10;
hence I = lim (lower_sum f,T) ; :: thesis: verum

end;

X2: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
lim (upper_sum f,T) = I

proof

let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies lim (upper_sum f,T) = I )
assume AS4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: lim (upper_sum f,T) = I
P1: ( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f ) by AS, AS4, INTEGRA4:9;
consider S being middle_volume_Sequence of f,T;

P2: now

let i be Element of NAT ; :: thesis: 0 <= ((upper_sum f,T) - (middle_sum f,S)) . i
(middle_sum f,S) . i <= (upper_sum f,T) . i by PX012, AS;
then ((middle_sum f,S) . i) - ((middle_sum f,S) . i) <= ((upper_sum f,T) . i) - ((middle_sum f,S) . i) by XREAL_1:11;
hence 0 <= ((upper_sum f,T) - (middle_sum f,S)) . i by VALUED_1:15; :: thesis: verum

end;

P3: middle_sum f,S is convergent by AS2, AS4;
then P4: (upper_sum f,T) - (middle_sum f,S) is convergent by P1, SEQ_2:25;
lim ((upper_sum f,T) - (middle_sum f,S)) = (lim (upper_sum f,T)) - (lim (middle_sum f,S)) by P1, P3, SEQ_2:26
.= (lim (upper_sum f,T)) - I by AS2, AS4 ;
then X10: 0 <= (lim (upper_sum f,T)) - I by SEQ_2:31, P2, P4;

now

let e1 be real number ; :: thesis: ( 0 < e1 implies (lim (upper_sum f,T)) - I <= e1 )
assume A41: 0 < e1 ; :: thesis: (lim (upper_sum f,T)) - I <= e1
reconsider e = e1 as Real by XREAL_0:def 1;
consider S being middle_volume_Sequence of f,T such that
N1: for i being Element of NAT holds ((upper_sum f,T) . i) - e <= (middle_sum f,S) . i by A41, PX03, AS;

N2: now

let i be Element of NAT ; :: thesis: ((upper_sum f,T) - (middle_sum f,S)) . i <= e
((upper_sum f,T) . i) - e <= (middle_sum f,S) . i by N1;
then (((upper_sum f,T) . i) - e) + e <= ((middle_sum f,S) . i) + e by XREAL_1:8;
then ((upper_sum f,T) . i) - ((middle_sum f,S) . i) <= (((middle_sum f,S) . i) + e) - ((middle_sum f,S) . i) by XREAL_1:11;
hence ((upper_sum f,T) - (middle_sum f,S)) . i <= e by VALUED_1:15; :: thesis: verum

end;

N3: middle_sum f,S is convergent by AS2, AS4;
then N4: (upper_sum f,T) - (middle_sum f,S) is convergent by P1, SEQ_2:25;
lim ((upper_sum f,T) - (middle_sum f,S)) = (lim (upper_sum f,T)) - (lim (middle_sum f,S)) by P1, N3, SEQ_2:26
.= (lim (upper_sum f,T)) - I by AS2, AS4 ;
hence (lim (upper_sum f,T)) - I <= e1 by N2, N4, PREPOWER:3; :: thesis: verum

end;

then (lim (upper_sum f,T)) - I = 0 by X10, XREAL_1:7;
hence lim (upper_sum f,T) = I ; :: thesis: verum

end;

now

let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0 )
assume XX: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0
thus (lim (upper_sum f,T)) - (lim (lower_sum f,T)) = (lim (upper_sum f,T)) - I by X1, XX
.= I - I by X2, XX
.= 0 ; :: thesis: verum

end;

hence f is integrable by INTEGRA4:12, AS; :: thesis: verum

end;

hence ( ex I being Real 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: verum