let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL
for u being continuous PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds
u is_RiemannStieltjes_integrable_with rho
let rho be Function of A,REAL; :: thesis: for u being continuous PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds
u is_RiemannStieltjes_integrable_with rho
let u be continuous PartFunc of REAL,REAL; :: thesis: ( rho is bounded_variation & dom u = A implies u is_RiemannStieltjes_integrable_with rho )
assume A1: ( rho is bounded_variation & dom u = A ) ; :: thesis: u is_RiemannStieltjes_integrable_with rho
A2: u | A is uniformly_continuous by A1, FCONT_2:11;
consider T0 being DivSequence of A such that
A3: ( delta T0 is convergent & lim (delta T0) = 0 ) by INTEGRA4:11;
set S0 = the middle_volume_Sequence of rho,u,T0;
set I = lim (middle_sum the middle_volume_Sequence of rho,u,T0);
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum S is convergent & lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) )

proof

let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum S is convergent & lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) )
let S be middle_volume_Sequence of rho,u,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum S is convergent & lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) ) )
assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum S is convergent & lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) )
hence middle_sum S is convergent by A1, A2, Th20; :: thesis: lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0)
consider T1 being DivSequence of A such that
A5: for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) by INTEGR20:15;
consider S1 being middle_volume_Sequence of rho,u,T1 such that
A6: for i being Nat holds
( S1 . (2 * i) = the middle_volume_Sequence of rho,u,T0 . i & S1 . ((2 * i) + 1) = S . i ) by A5, Th21;
( delta T1 is convergent & lim (delta T1) = 0 ) by A3, A4, A5, INTEGR20:16;
then A7: middle_sum S1 is convergent by A1, A2, Th20;
A8: for i being Nat holds
( (middle_sum S1) . (2 * i) = (middle_sum the middle_volume_Sequence of rho,u,T0) . i & (middle_sum S1) . ((2 * i) + 1) = (middle_sum S) . i )

proof

let i be Nat; :: thesis: ( (middle_sum S1) . (2 * i) = (middle_sum the middle_volume_Sequence of rho,u,T0) . i & (middle_sum S1) . ((2 * i) + 1) = (middle_sum S) . i )
reconsider S1 = S1 as middle_volume_Sequence of rho,u,T1 ;
( S1 . (2 * i) = the middle_volume_Sequence of rho,u,T0 . i & T1 . (2 * i) = T0 . i & S1 . ((2 * i) + 1) = S . i & T1 . ((2 * i) + 1) = T . i ) by A5, A6;
then ( (middle_sum S1) . (2 * i) = Sum ( the middle_volume_Sequence of rho,u,T0 . i) & (middle_sum S1) . ((2 * i) + 1) = Sum (S . i) ) by INTEGR22:def 7;
hence ( (middle_sum S1) . (2 * i) = (middle_sum the middle_volume_Sequence of rho,u,T0) . i & (middle_sum S1) . ((2 * i) + 1) = (middle_sum S) . i ) by INTEGR22:def 7; :: thesis: verum

end;

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

end;

hence u is_RiemannStieltjes_integrable_with rho by INTEGR22:def 8; :: thesis: verum