let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded holds
( f is integrable iff 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 f be Function of A,REAL; :: thesis: ( f | A is bounded implies ( f is integrable iff 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 ) )
assume A1: f | A is bounded ; :: thesis: ( f is integrable iff 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 )
A2: ( f is integrable implies 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 )

proof

assume A3: f is integrable ; :: 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
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

proof

A4: upper_integral f = lower_integral f by A3, INTEGRA1:def 16;
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 that
A5: delta T is convergent and
A6: lim (delta T) = 0 ; :: thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0
A7: lim (lower_sum (f,T)) = lower_integral f by A1, A5, A6, Th8;
lim (upper_sum (f,T)) = upper_integral f by A1, A5, A6, Th9;
hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A7, A4; :: thesis: verum

end;

hence 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 ; :: thesis: verum

end;

( ( 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 ) implies f is integrable )

proof

consider T being DivSequence of A such that
A8: delta T is convergent and
A9: lim (delta T) = 0 by Th11;
assume 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 ; :: thesis: f is integrable
then (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A8, A9;
then (upper_integral f) - (lim (lower_sum (f,T))) = 0 by A1, A8, A9, Th9;
then A10: (upper_integral f) - (lower_integral f) = 0 by A1, A8, A9, Th8;
A11: f is lower_integrable by A1, Th10;
f is upper_integrable by A1, Th10;
hence f is integrable by A11, A10, INTEGRA1:def 16; :: thesis: verum

end;

hence ( f is integrable iff 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 ) by A2; :: thesis: verum