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 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)).| ) ) ) )
let rho be Function of A,REAL; :: thesis: 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)).| ) ) ) )
let T, S be Division of A; :: thesis: ( rho is bounded_variation implies 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)).| ) ) ) ) )
assume A1: rho is bounded_variation ; :: thesis: 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)).| ) ) ) )
defpred S₁[ Nat, object ] means ex p being FinSequence of REAL st
( $2 = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,$1))),rho)).| ) );
A2: for j being Nat st j in Seg (len S) holds
ex x being Element of REAL st S₁[j,x]

proof

let j be Nat; :: thesis: ( j in Seg (len S) implies ex x being Element of REAL st S₁[j,x] )
assume j in Seg (len S) ; :: thesis: ex x being Element of REAL st S₁[j,x]
defpred S₂[ Nat, object ] means $2 = |.(vol (((divset (T,$1)) /\ (divset (S,j))),rho)).|;
A3: for i being Nat st i in Seg (len T) holds
ex y being Element of REAL st S₂[i,y]

proof

let i be Nat; :: thesis: ( i in Seg (len T) implies ex y being Element of REAL st S₂[i,y] )
assume i in Seg (len T) ; :: thesis: ex y being Element of REAL st S₂[i,y]
|.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S₂[i,y] ; :: thesis: verum

end;

consider p being FinSequence of REAL such that
A4: ( dom p = Seg (len T) & ( for i being Nat st i in Seg (len T) holds
S₂[i,p . i] ) ) from FINSEQ_1:sch 5(A3);
reconsider x = Sum p as Element of REAL by XREAL_0:def 1;
Z2: dom T = Seg (len T) by FINSEQ_1:def 3;
len p = len T by A4, FINSEQ_1:def 3;
then S₁[j,x] by A4, Z2;
hence ex x being Element of REAL st S₁[j,x] ; :: thesis: verum

end;

consider ST being FinSequence of REAL such that
A5: ( dom ST = Seg (len S) & ( for j being Nat st j in Seg (len S) holds
S₁[j,ST . j] ) ) from FINSEQ_1:sch 5(A2);
take ST ; :: thesis: ( 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)).| ) ) ) )
thus A6: len ST = len S by A5, FINSEQ_1:def 3; :: thesis: ( 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)).| ) ) ) )
a6: dom ST = dom S by A5, FINSEQ_1:def 3;
then consider H being Division of A, F being var_volume of rho,H such that
A7: Sum ST = Sum F by A1, A5, A6, Lm2;
thus ( 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)).| ) ) ) ) by A1, A5, A7, INTEGR22:5, a6; :: thesis: verum