:: deftheorem defines is_RiemannStieltjes_integrable_with INTEGR22:def 8 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL holds
( u is_RiemannStieltjes_integrable_with rho iff ex I being Real st
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) = I ) );