:: deftheorem defines bounded_variation INTEGR22:def 3 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL holds
( rho is bounded_variation iff ex d being Real st
( 0 < d & ( for t being Division of A
for F being var_volume of rho,t holds Sum F <= d ) ) );