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

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