for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for T, S being Division of A st rho is bounded_variation holds
ex ST being FinSequence of REAL st
( len ST = len S & Sum ST <= total_vd rho & ( for j being Nat st j in dom S holds
ex p being FinSequence of REAL st
( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) )