let A be 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

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

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