let A be non empty closed_interval Subset of REAL; 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; 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; ( 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
; 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 S1[ 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 S1[j,x]
proof
let j be
Nat;
( j in Seg (len S) implies ex x being Element of REAL st S1[j,x] )
assume
j in Seg (len S)
;
ex x being Element of REAL st S1[j,x]
defpred S2[
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
S2[
i,
y]
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
S2[
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
S1[
j,
x]
by A4, Z2;
hence
ex
x being
Element of
REAL st
S1[
j,
x]
;
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
S1[j,ST . j] ) )
from FINSEQ_1:sch 5(A2);
take
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)).| ) ) ) )
thus A6:
len ST = len S
by A5, FINSEQ_1:def 3; ( 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; verum