let A be non empty 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 A1: 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 ) )

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 A2: 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 A1, A2, Th9; :: thesis: verum

end;

dom f = A by FUNCT_2:def 1;
then A3: f | A is bounded by A1, RELAT_1:69;

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
A4: 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 ) ;
A5: 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 )
set S = the middle_volume_Sequence of f,T;

A6: now

let i be Element of NAT ; :: thesis: 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i
(middle_sum (f, the middle_volume_Sequence of f,T)) . i <= (upper_sum (f,T)) . i by A3, Th6;
then ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) <= ((upper_sum (f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) by XREAL_1:9;
hence 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i by VALUED_1:15; :: thesis: verum

end;

assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: lim (upper_sum (f,T)) = I
then A8: upper_sum (f,T) is convergent by A3, INTEGRA4:9;

A9: now

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

A11: 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 A10;
then (((upper_sum (f,T)) . i) - e) + e <= ((middle_sum (f,S)) . i) + e by XREAL_1:6;
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:9;
hence ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e by VALUED_1:15; :: thesis: verum

end;

A12: middle_sum (f,S) is convergent by A4, A7;
then A13: (upper_sum (f,T)) - (middle_sum (f,S)) is convergent by A8;
lim ((upper_sum (f,T)) - (middle_sum (f,S))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f,S))) by A8, A12, SEQ_2:12
.= (lim (upper_sum (f,T))) - I by A4, A7 ;
hence (lim (upper_sum (f,T))) - I <= e1 by A11, A13, PREPOWER:2; :: thesis: verum

end;

A14: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A7;
then A15: (upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T)) is convergent by A8;
lim ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f, the middle_volume_Sequence of f,T))) by A8, A14, SEQ_2:12
.= (lim (upper_sum (f,T))) - I by A4, A7 ;
then 0 <= (lim (upper_sum (f,T))) - I by A6, A15, SEQ_2:17;
then (lim (upper_sum (f,T))) - I = 0 by A9, XREAL_1:5;
hence lim (upper_sum (f,T)) = I ; :: thesis: verum

end;

A16: 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)) )
set S = the middle_volume_Sequence of f,T;

A17: now

let i be Element of NAT ; :: thesis: 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i
(lower_sum (f,T)) . i <= (middle_sum (f, the middle_volume_Sequence of f,T)) . i by A3, Th5;
then ((lower_sum (f,T)) . i) - ((lower_sum (f,T)) . i) <= ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((lower_sum (f,T)) . i) by XREAL_1:9;
hence 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i by VALUED_1:15; :: thesis: verum

end;

assume A18: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: I = lim (lower_sum (f,T))
then A19: lower_sum (f,T) is convergent by A3, INTEGRA4:8;

A20: now

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

A22: 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 A21;
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:9;
hence ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e by VALUED_1:15; :: thesis: verum

end;

A23: middle_sum (f,S) is convergent by A4, A18;
then A24: (middle_sum (f,S)) - (lower_sum (f,T)) is convergent by A19;
lim ((middle_sum (f,S)) - (lower_sum (f,T))) = (lim (middle_sum (f,S))) - (lim (lower_sum (f,T))) by A19, A23, SEQ_2:12
.= I - (lim (lower_sum (f,T))) by A4, A18 ;
hence I - (lim (lower_sum (f,T))) <= e1 by A22, A24, PREPOWER:2; :: thesis: verum

end;

A25: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A18;
then A26: (middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T)) is convergent by A19;
lim ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) = (lim (middle_sum (f, the middle_volume_Sequence of f,T))) - (lim (lower_sum (f,T))) by A19, A25, SEQ_2:12
.= I - (lim (lower_sum (f,T))) by A4, A18 ;
then 0 <= I - (lim (lower_sum (f,T))) by A17, A26, SEQ_2:17;
then I - (lim (lower_sum (f,T))) = 0 by A20, XREAL_1:5;
hence I = lim (lower_sum (f,T)) ; :: 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 A27: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0
hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = (lim (upper_sum (f,T))) - I by A16
.= I - I by A5, A27
.= 0 ;
:: thesis: verum

end;

hence f is integrable by A3, INTEGRA4:12; :: 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