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 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 )
reconsider I = integral f as Real ;
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 (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;

A3: f | A is bounded by A1;

now :: 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 )

given 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 ) ; :: thesis: f is integrable
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 :: thesis: for i being Nat holds 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i

let i be Nat; :: thesis: 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i
A7: i in NAT by ORDINAL1:def 12;
(middle_sum (f, the middle_volume_Sequence of f,T)) . i <= (upper_sum (f,T)) . i by A3, Th6, A7;
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, A7; :: thesis: verum

end;

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

A10: now :: thesis: for e1 being Real st 0 < e1 holds
(lim (upper_sum (f,T))) - I <= e1

let e1 be Real; :: thesis: ( 0 < e1 implies (lim (upper_sum (f,T))) - I <= e1 )
reconsider e = e1 as Element of 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
A11: for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A3, Th8;

A12: now :: thesis: for i being Nat holds ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e

let i be Nat; :: thesis: ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e
A13: i in NAT by ORDINAL1:def 12;
((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A11, A13;
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, A13; :: thesis: verum

end;

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

end;

A16: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A8;
then A17: (upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T)) is convergent by A9;
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 A9, A16, SEQ_2:12
.= (lim (upper_sum (f,T))) - I by A4, A8 ;
then 0 <= (lim (upper_sum (f,T))) - I by A6, A17, SEQ_2:17;
then (lim (upper_sum (f,T))) - I = 0 by A10, XREAL_1:5;
hence lim (upper_sum (f,T)) = I ; :: thesis: verum

end;

A18: 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;

A19: now :: thesis: for i being Nat holds 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i

let i be Nat; :: thesis: 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i
A20: i in NAT by ORDINAL1:def 12;
(lower_sum (f,T)) . i <= (middle_sum (f, the middle_volume_Sequence of f,T)) . i by A3, Th5, A20;
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, A20; :: thesis: verum

end;

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

A23: now :: thesis: for e1 being Real st 0 < e1 holds
I - (lim (lower_sum (f,T))) <= e1

let e1 be Real; :: thesis: ( 0 < e1 implies I - (lim (lower_sum (f,T))) <= e1 )
reconsider e = e1 as Element of 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
A24: for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A3, Th7;

A25: now :: thesis: for i being Nat holds ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e

let i be Nat; :: thesis: ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e
A26: i in NAT by ORDINAL1:def 12;
(middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A24, A26;
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, A26; :: thesis: verum

end;

A27: middle_sum (f,S) is convergent by A4, A21;
then A28: (middle_sum (f,S)) - (lower_sum (f,T)) is convergent by A22;
lim ((middle_sum (f,S)) - (lower_sum (f,T))) = (lim (middle_sum (f,S))) - (lim (lower_sum (f,T))) by A22, A27, SEQ_2:12
.= I - (lim (lower_sum (f,T))) by A4, A21 ;
hence I - (lim (lower_sum (f,T))) <= e1 by A25, A28, PREPOWER:2; :: thesis: verum

end;

A29: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A21;
then A30: (middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T)) is convergent by A22;
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 A22, A29, SEQ_2:12
.= I - (lim (lower_sum (f,T))) by A4, A21 ;
then 0 <= I - (lim (lower_sum (f,T))) by A19, A30, SEQ_2:17;
then I - (lim (lower_sum (f,T))) = 0 by A23, XREAL_1:5;
hence I = lim (lower_sum (f,T)) ; :: thesis: verum

end;

now :: thesis: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0

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 A31: ( 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 A18
.= I - I by A5, A31
.= 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