let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL
for T, S being Division of A
for ST being FinSequence of REAL st rho is bounded_variation & len ST = len S & ( 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)).| ) ) ) holds
ex H being Division of A ex F being var_volume of rho,H st Sum ST = Sum F
let rho be Function of A,REAL; :: thesis: for T, S being Division of A
for ST being FinSequence of REAL st rho is bounded_variation & len ST = len S & ( 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)).| ) ) ) holds
ex H being Division of A ex F being var_volume of rho,H st Sum ST = Sum F
let T, S be Division of A; :: thesis: for ST being FinSequence of REAL st rho is bounded_variation & len ST = len S & ( 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)).| ) ) ) holds
ex H being Division of A ex F being var_volume of rho,H st Sum ST = Sum F
let ST be FinSequence of REAL ; :: thesis: ( rho is bounded_variation & len ST = len S & ( 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)).| ) ) ) implies ex H being Division of A ex F being var_volume of rho,H st Sum ST = Sum F )
assume A1: ( rho is bounded_variation & len ST = len S & ( 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)).| ) ) ) ) ; :: thesis: ex H being Division of A ex F being var_volume of rho,H st Sum ST = Sum F
( A c= A & lower_bound A = lower_bound A ) ;
hence ex H being Division of A ex F being var_volume of rho,H st Sum ST = Sum F by A1, Th18; :: thesis: verum