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

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 )
consider S being middle_volume_Sequence of f,T;

A6: 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 A3, Th6;
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;

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

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

end;

A14: middle_sum f,S is convergent by A4, A7;
then A15: (upper_sum f,T) - (middle_sum f,S) is convergent by A8, SEQ_2:25;
lim ((upper_sum f,T) - (middle_sum f,S)) = (lim (upper_sum f,T)) - (lim (middle_sum f,S)) by A8, A14, SEQ_2:26
.= (lim (upper_sum f,T)) - I by A4, A7 ;
then 0 <= (lim (upper_sum f,T)) - I by A6, A15, SEQ_2:31;
then (lim (upper_sum f,T)) - I = 0 by A9, XREAL_1:7;
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) )
consider S being middle_volume_Sequence of f,T;

A17: 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 A3, Th5;
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;

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:11;
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, SEQ_2:25;
lim ((middle_sum f,S) - (lower_sum f,T)) = (lim (middle_sum f,S)) - (lim (lower_sum f,T)) by A19, A23, SEQ_2:26
.= I - (lim (lower_sum f,T)) by A4, A18 ;
hence I - (lim (lower_sum f,T)) <= e1 by A22, A24, PREPOWER:3; :: thesis: verum

end;

A25: middle_sum f,S is convergent by A4, A18;
then A26: (middle_sum f,S) - (lower_sum f,T) is convergent by A19, SEQ_2:25;
lim ((middle_sum f,S) - (lower_sum f,T)) = (lim (middle_sum f,S)) - (lim (lower_sum f,T)) by A19, A25, SEQ_2:26
.= I - (lim (lower_sum f,T)) by A4, A18 ;
then 0 <= I - (lim (lower_sum f,T)) by A17, A26, SEQ_2:31;
then I - (lim (lower_sum f,T)) = 0 by A20, XREAL_1:7;
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