let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL
for T being Division of A st rho is bounded_variation holds
for F being var_volume of rho,T holds Sum F <= total_vd rho
let rho be Function of A,REAL; :: thesis: for T being Division of A st rho is bounded_variation holds
for F being var_volume of rho,T holds Sum F <= total_vd rho
let T be Division of A; :: thesis: ( rho is bounded_variation implies for F being var_volume of rho,T holds Sum F <= total_vd rho )
assume rho is bounded_variation ; :: thesis: for F being var_volume of rho,T holds Sum F <= total_vd rho
then consider VD being non empty Subset of REAL such that
A1: VD is bounded_above and
A2: VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } and
A3: total_vd rho = upper_bound VD by DeftotalVD;
let F be var_volume of rho,T; :: thesis: Sum F <= total_vd rho
Sum F in VD by A2;
hence Sum F <= total_vd rho by A1, SEQ_4:def 1, A3; :: thesis: verum