let a, b be Real; :: thesis: for X being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f holds
f is_integrable_on ['a,b']
let X be RealBanachSpace; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f holds
f is_integrable_on ['a,b']
let f be continuous PartFunc of REAL, the carrier of X; :: thesis: ( a <= b & ['a,b'] c= dom f implies f is_integrable_on ['a,b'] )
set A = ['a,b'];
assume A1: ( a <= b & ['a,b'] c= dom f ) ; :: thesis: f is_integrable_on ['a,b']
then reconsider h = f | ['a,b'] as Function of ['a,b'], the carrier of X by Lm1;
A2: f | ['a,b'] is uniformly_continuous by A1, Th3;
consider T0 being DivSequence of ['a,b'] such that
A3: ( delta T0 is convergent & lim (delta T0) = 0 ) by INTEGRA4:11;
set S0 = the middle_volume_Sequence of h,T0;
set I = lim (middle_sum (h, the middle_volume_Sequence of h,T0));
for T being DivSequence of ['a,b']
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) )

proof

let T be DivSequence of ['a,b']; :: thesis: for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) )
let S be middle_volume_Sequence of h,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) ) )
assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) )
hence middle_sum (h,S) is convergent by A2, Th13; :: thesis: lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0))
consider T1 being DivSequence of ['a,b'] such that
A5: for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) by Th15;
consider S1 being middle_volume_Sequence of h,T1 such that
A6: for i being Nat holds
( S1 . (2 * i) = the middle_volume_Sequence of h,T0 . i & S1 . ((2 * i) + 1) = S . i ) by A5, Th17;
( delta T1 is convergent & lim (delta T1) = 0 ) by A4, A5, A3, Th16;
then A7: middle_sum (h,S1) is convergent by A2, Th13;
A8: for i being Nat holds
( (middle_sum (h,S1)) . (2 * i) = (middle_sum (h, the middle_volume_Sequence of h,T0)) . i & (middle_sum (h,S1)) . ((2 * i) + 1) = (middle_sum (h,S)) . i )

proof

let i be Nat; :: thesis: ( (middle_sum (h,S1)) . (2 * i) = (middle_sum (h, the middle_volume_Sequence of h,T0)) . i & (middle_sum (h,S1)) . ((2 * i) + 1) = (middle_sum (h,S)) . i )
reconsider S1 = S1 as middle_volume_Sequence of h,T1 ;
( (middle_sum (h,S1)) . (2 * i) = middle_sum (h,(S1 . (2 * i))) & (middle_sum (h,S1)) . ((2 * i) + 1) = middle_sum (h,(S1 . ((2 * i) + 1))) ) by INTEGR18:def 4;
then ( (middle_sum (h,S1)) . (2 * i) = middle_sum (h,( the middle_volume_Sequence of h,T0 . i)) & (middle_sum (h,S1)) . ((2 * i) + 1) = middle_sum (h,(S . i)) ) by A6;
hence ( (middle_sum (h,S1)) . (2 * i) = (middle_sum (h, the middle_volume_Sequence of h,T0)) . i & (middle_sum (h,S1)) . ((2 * i) + 1) = (middle_sum (h,S)) . i ) by INTEGR18:def 4; :: thesis: verum

end;

lim (middle_sum (h,S)) = lim (middle_sum (h,S1)) by A7, A8, Th18;
hence lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) by A7, A8, Th18; :: thesis: verum

end;

then h is integrable ;
hence f is_integrable_on ['a,b'] ; :: thesis: verum