let A be non empty closed_interval Subset of REAL; for rho, rho1, rho2 being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & rho2 is bounded_variation & dom u = A & rho = rho1 - rho2 & u is_RiemannStieltjes_integrable_with rho1 & u is_RiemannStieltjes_integrable_with rho2 holds
( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2)) )
let rho, rho1, rho2 be Function of A,REAL; for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & rho2 is bounded_variation & dom u = A & rho = rho1 - rho2 & u is_RiemannStieltjes_integrable_with rho1 & u is_RiemannStieltjes_integrable_with rho2 holds
( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2)) )
let u be PartFunc of REAL,REAL; ( rho is bounded_variation & rho1 is bounded_variation & rho2 is bounded_variation & dom u = A & rho = rho1 - rho2 & u is_RiemannStieltjes_integrable_with rho1 & u is_RiemannStieltjes_integrable_with rho2 implies ( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2)) ) )
assume A1:
( rho is bounded_variation & rho1 is bounded_variation & rho2 is bounded_variation & dom u = A & rho = rho1 - rho2 & u is_RiemannStieltjes_integrable_with rho1 & u is_RiemannStieltjes_integrable_with rho2 )
; ( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2)) )
A3:
now for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho1)) - (integral (u,rho2)) )let T be
DivSequence of
A;
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho1)) - (integral (u,rho2)) )let S be
middle_volume_Sequence of
rho,
u,
T;
( delta T is convergent & lim (delta T) = 0 implies ( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho1)) - (integral (u,rho2)) ) )assume A4:
(
delta T is
convergent &
lim (delta T) = 0 )
;
( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho1)) - (integral (u,rho2)) )defpred S1[
Element of
NAT ,
set ]
means ex
p being
FinSequence of
REAL st
(
p = $2 &
len p = len (T . $1) & ( for
i being
Nat st
i in dom (T . $1) holds
(
p . i in dom (u | (divset ((T . $1),i))) & ex
z being
Real st
(
z = (u | (divset ((T . $1),i))) . (p . i) &
(S . $1) . i = z * (vol ((divset ((T . $1),i)),rho)) ) ) ) );
A5:
for
k being
Element of
NAT ex
p being
Element of
REAL * st
S1[
k,
p]
proof
let k be
Element of
NAT ;
ex p being Element of REAL * st S1[k,p]
defpred S2[
Nat,
set ]
means ( $2
in dom (u | (divset ((T . k),$1))) & ex
c being
Real st
(
c = (u | (divset ((T . k),$1))) . $2 &
(S . k) . $1
= c * (vol ((divset ((T . k),$1)),rho)) ) );
A6:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A7:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
x being
Element of
REAL st
S2[
i,
x]
proof
let i be
Nat;
( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume
i in Seg (len (T . k))
;
ex x being Element of REAL st S2[i,x]
then
i in dom (T . k)
by FINSEQ_1:def 3;
then consider c being
Real such that A8:
(
c in rng (u | (divset ((T . k),i))) &
(S . k) . i = c * (vol ((divset ((T . k),i)),rho)) )
by Def1, A1;
consider x being
object such that A9:
(
x in dom (u | (divset ((T . k),i))) &
c = (u | (divset ((T . k),i))) . x )
by A8, FUNCT_1:def 3;
reconsider x =
x as
Element of
REAL by A9;
take
x
;
S2[i,x]
thus
S2[
i,
x]
by A8, A9;
verum
end;
consider p being
FinSequence of
REAL such that A10:
(
dom p = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S2[
i,
p . i] ) )
from FINSEQ_1:sch 5(A7);
take
p
;
( p is Element of REAL * & S1[k,p] )
len p = len (T . k)
by A10, FINSEQ_1:def 3;
hence
(
p is
Element of
REAL * &
S1[
k,
p] )
by A10, A6, FINSEQ_1:def 11;
verum
end; consider F being
sequence of
(REAL *) such that A11:
for
x being
Element of
NAT holds
S1[
x,
F . x]
from FUNCT_2:sch 3(A5);
defpred S2[
Element of
NAT ,
set ]
means ex
q being
middle_volume of
rho1,
u,
T . $1 st
(
q = $2 & ( for
i being
Nat st
i in dom (T . $1) holds
ex
z being
Real st
(
(F . $1) . i in dom (u | (divset ((T . $1),i))) &
z = (u | (divset ((T . $1),i))) . ((F . $1) . i) &
q . i = z * (vol ((divset ((T . $1),i)),rho1)) ) ) );
A12:
for
k being
Element of
NAT ex
y being
Element of
REAL * st
S2[
k,
y]
proof
let k be
Element of
NAT ;
ex y being Element of REAL * st S2[k,y]
defpred S3[
Nat,
set ]
means ex
c being
Real st
(
(F . k) . $1
in dom (u | (divset ((T . k),$1))) &
c = (u | (divset ((T . k),$1))) . ((F . k) . $1) & $2
= c * (vol ((divset ((T . k),$1)),rho1)) );
A13:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A14:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
x being
Element of
REAL st
S3[
i,
x]
proof
let i be
Nat;
( i in Seg (len (T . k)) implies ex x being Element of REAL st S3[i,x] )
assume
i in Seg (len (T . k))
;
ex x being Element of REAL st S3[i,x]
then A15:
i in dom (T . k)
by FINSEQ_1:def 3;
consider p being
FinSequence of
REAL such that A16:
(
p = F . k &
len p = len (T . k) & ( for
i being
Nat st
i in dom (T . k) holds
(
p . i in dom (u | (divset ((T . k),i))) & ex
z being
Real st
(
z = (u | (divset ((T . k),i))) . (p . i) &
(S . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) )
by A11;
p . i in dom (u | (divset ((T . k),i)))
by A15, A16;
then
(u | (divset ((T . k),i))) . (p . i) in rng (u | (divset ((T . k),i)))
by FUNCT_1:3;
then reconsider x =
(u | (divset ((T . k),i))) . (p . i) as
Element of
REAL ;
x * (vol ((divset ((T . k),i)),rho1)) is
Element of
REAL
by XREAL_0:def 1;
hence
ex
x being
Element of
REAL st
S3[
i,
x]
by A16, A15;
verum
end;
consider q being
FinSequence of
REAL such that A19:
(
dom q = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S3[
i,
q . i] ) )
from FINSEQ_1:sch 5(A14);
A20:
len q = len (T . k)
by A19, FINSEQ_1:def 3;
now for i being Nat st i in dom (T . k) holds
ex c being Real st
( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho1)) )let i be
Nat;
( i in dom (T . k) implies ex c being Real st
( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho1)) ) )assume
i in dom (T . k)
;
ex c being Real st
( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho1)) )then
i in Seg (len (T . k))
by FINSEQ_1:def 3;
then consider c being
Real such that A21:
(
(F . k) . i in dom (u | (divset ((T . k),i))) &
c = (u | (divset ((T . k),i))) . ((F . k) . i) &
q . i = c * (vol ((divset ((T . k),i)),rho1)) )
by A19;
thus
ex
c being
Real st
(
c in rng (u | (divset ((T . k),i))) &
q . i = c * (vol ((divset ((T . k),i)),rho1)) )
by A21, FUNCT_1:3;
verum end;
then reconsider q =
q as
middle_volume of
rho1,
u,
T . k by A20, Def1, A1;
q is
Element of
REAL *
by FINSEQ_1:def 11;
hence
ex
y being
Element of
REAL * st
S2[
k,
y]
by A13, A19;
verum
end; consider Sf being
sequence of
(REAL *) such that A22:
for
x being
Element of
NAT holds
S2[
x,
Sf . x]
from FUNCT_2:sch 3(A12);
now for k being Element of NAT holds Sf . k is middle_volume of rho1,u,T . klet k be
Element of
NAT ;
Sf . k is middle_volume of rho1,u,T . k
ex
q being
middle_volume of
rho1,
u,
T . k st
(
q = Sf . k & ( for
i being
Nat st
i in dom (T . k) holds
ex
z being
Real st
(
(F . k) . i in dom (u | (divset ((T . k),i))) &
z = (u | (divset ((T . k),i))) . ((F . k) . i) &
q . i = z * (vol ((divset ((T . k),i)),rho1)) ) ) )
by A22;
hence
Sf . k is
middle_volume of
rho1,
u,
T . k
;
verum end; then reconsider Sf =
Sf as
middle_volume_Sequence of
rho1,
u,
T by Def3;
defpred S3[
Element of
NAT ,
set ]
means ex
q being
middle_volume of
rho2,
u,
T . $1 st
(
q = $2 & ( for
i being
Nat st
i in dom (T . $1) holds
ex
z being
Real st
(
(F . $1) . i in dom (u | (divset ((T . $1),i))) &
z = (u | (divset ((T . $1),i))) . ((F . $1) . i) &
q . i = z * (vol ((divset ((T . $1),i)),rho2)) ) ) );
A23:
for
k being
Element of
NAT ex
y being
Element of
REAL * st
S3[
k,
y]
proof
let k be
Element of
NAT ;
ex y being Element of REAL * st S3[k,y]
defpred S4[
Nat,
set ]
means ex
c being
Real st
(
(F . k) . $1
in dom (u | (divset ((T . k),$1))) &
c = (u | (divset ((T . k),$1))) . ((F . k) . $1) & $2
= c * (vol ((divset ((T . k),$1)),rho2)) );
A24:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A25:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
x being
Element of
REAL st
S4[
i,
x]
proof
let i be
Nat;
( i in Seg (len (T . k)) implies ex x being Element of REAL st S4[i,x] )
assume
i in Seg (len (T . k))
;
ex x being Element of REAL st S4[i,x]
then A26:
i in dom (T . k)
by FINSEQ_1:def 3;
consider p being
FinSequence of
REAL such that A27:
(
p = F . k &
len p = len (T . k) & ( for
i being
Nat st
i in dom (T . k) holds
(
p . i in dom (u | (divset ((T . k),i))) & ex
z being
Real st
(
z = (u | (divset ((T . k),i))) . (p . i) &
(S . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) )
by A11;
p . i in dom (u | (divset ((T . k),i)))
by A26, A27;
then
(u | (divset ((T . k),i))) . (p . i) in rng (u | (divset ((T . k),i)))
by FUNCT_1:3;
then reconsider x =
(u | (divset ((T . k),i))) . (p . i) as
Element of
REAL ;
x * (vol ((divset ((T . k),i)),rho2)) is
Element of
REAL
by XREAL_0:def 1;
hence
ex
x being
Element of
REAL st
S4[
i,
x]
by A27, A26;
verum
end;
consider q being
FinSequence of
REAL such that A30:
(
dom q = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S4[
i,
q . i] ) )
from FINSEQ_1:sch 5(A25);
A31:
len q = len (T . k)
by A30, FINSEQ_1:def 3;
now for i being Nat st i in dom (T . k) holds
ex c being Real st
( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho2)) )let i be
Nat;
( i in dom (T . k) implies ex c being Real st
( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho2)) ) )assume
i in dom (T . k)
;
ex c being Real st
( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho2)) )then
i in Seg (len (T . k))
by FINSEQ_1:def 3;
then consider c being
Real such that A32:
(
(F . k) . i in dom (u | (divset ((T . k),i))) &
c = (u | (divset ((T . k),i))) . ((F . k) . i) &
q . i = c * (vol ((divset ((T . k),i)),rho2)) )
by A30;
thus
ex
c being
Real st
(
c in rng (u | (divset ((T . k),i))) &
q . i = c * (vol ((divset ((T . k),i)),rho2)) )
by A32, FUNCT_1:3;
verum end;
then reconsider q =
q as
middle_volume of
rho2,
u,
T . k by A31, Def1, A1;
q is
Element of
REAL *
by FINSEQ_1:def 11;
hence
ex
y being
Element of
REAL * st
S3[
k,
y]
by A24, A30;
verum
end; consider Sg being
sequence of
(REAL *) such that A33:
for
x being
Element of
NAT holds
S3[
x,
Sg . x]
from FUNCT_2:sch 3(A23);
now for k being Element of NAT holds Sg . k is middle_volume of rho2,u,T . klet k be
Element of
NAT ;
Sg . k is middle_volume of rho2,u,T . k
ex
q being
middle_volume of
rho2,
u,
T . k st
(
q = Sg . k & ( for
i being
Nat st
i in dom (T . k) holds
ex
z being
Real st
(
(F . k) . i in dom (u | (divset ((T . k),i))) &
z = (u | (divset ((T . k),i))) . ((F . k) . i) &
q . i = z * (vol ((divset ((T . k),i)),rho2)) ) ) )
by A33;
hence
Sg . k is
middle_volume of
rho2,
u,
T . k
;
verum end; then reconsider Sg =
Sg as
middle_volume_Sequence of
rho2,
u,
T by Def3;
A34:
(
middle_sum Sf is
convergent &
lim (middle_sum Sf) = integral (
u,
rho1) )
by A1, A4, Def6;
A35:
(
middle_sum Sg is
convergent &
lim (middle_sum Sg) = integral (
u,
rho2) )
by A1, A4, Def6;
A36:
(middle_sum Sf) - (middle_sum Sg) = middle_sum S
proof
now for n being Nat holds ((middle_sum Sf) . n) + ((- (middle_sum Sg)) . n) = (middle_sum S) . nlet n be
Nat;
((middle_sum Sf) . n) + ((- (middle_sum Sg)) . n) = (middle_sum S) . nA37:
n in NAT
by ORDINAL1:def 12;
consider p being
FinSequence of
REAL such that A38:
(
p = F . n &
len p = len (T . n) & ( for
i being
Nat st
i in dom (T . n) holds
(
p . i in dom (u | (divset ((T . n),i))) & ex
z being
Real st
(
z = (u | (divset ((T . n),i))) . (p . i) &
(S . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) )
by A11, A37;
consider q being
middle_volume of
rho1,
u,
T . n such that A39:
(
q = Sf . n & ( for
i being
Nat st
i in dom (T . n) holds
ex
z being
Real st
(
(F . n) . i in dom (u | (divset ((T . n),i))) &
z = (u | (divset ((T . n),i))) . ((F . n) . i) &
q . i = z * (vol ((divset ((T . n),i)),rho1)) ) ) )
by A22, A37;
consider r being
middle_volume of
rho2,
u,
T . n such that A40:
(
r = Sg . n & ( for
i being
Nat st
i in dom (T . n) holds
ex
z being
Real st
(
(F . n) . i in dom (u | (divset ((T . n),i))) &
z = (u | (divset ((T . n),i))) . ((F . n) . i) &
r . i = z * (vol ((divset ((T . n),i)),rho2)) ) ) )
by A33, A37;
A41:
(
len (Sf . n) = len (T . n) &
len (Sg . n) = len (T . n) &
len (S . n) = len (T . n) )
by A1, Def1;
then A42:
(
dom (Sf . n) = dom (T . n) &
dom (Sg . n) = dom (T . n) &
dom (S . n) = dom (T . n) )
by FINSEQ_3:29;
B42:
dom (S . n) =
(dom (Sf . n)) /\ (dom (Sg . n))
by A42
.=
dom ((Sf . n) - (Sg . n))
by VALUED_1:12
;
now for j being object st j in dom (S . n) holds
(S . n) . j = ((Sf . n) . j) - ((Sg . n) . j)let j be
object ;
( j in dom (S . n) implies (S . n) . j = ((Sf . n) . j) - ((Sg . n) . j) )assume A43:
j in dom (S . n)
;
(S . n) . j = ((Sf . n) . j) - ((Sg . n) . j)then reconsider i =
j as
Nat ;
consider t being
Real such that A44:
(
t = (u | (divset ((T . n),i))) . ((F . n) . i) &
(S . n) . i = t * (vol ((divset ((T . n),i)),rho)) )
by A43, A42, A38;
consider z being
Real such that A45:
(
(F . n) . i in dom (u | (divset ((T . n),i))) &
z = (u | (divset ((T . n),i))) . ((F . n) . i) &
q . i = z * (vol ((divset ((T . n),i)),rho1)) )
by A39, A43, A42;
consider w1 being
Real such that A46:
(
(F . n) . i in dom (u | (divset ((T . n),i))) &
w1 = (u | (divset ((T . n),i))) . ((F . n) . i) &
r . i = w1 * (vol ((divset ((T . n),i)),rho2)) )
by A40, A43, A42;
i in dom (T . n)
by A41, FINSEQ_3:29, A43;
then
vol (
(divset ((T . n),i)),
rho)
= (vol ((divset ((T . n),i)),rho1)) - (vol ((divset ((T . n),i)),rho2))
by A1, Lm7A, INTEGRA1:8;
hence
(S . n) . j = ((Sf . n) . j) - ((Sg . n) . j)
by A45, A39, A46, A40, A44;
verum end; then A57:
(Sf . n) - (Sg . n) = S . n
by B42, VALUED_1:14;
set k =
len (T . n);
X1:
Sf . n is
Element of
(len (T . n)) -tuples_on REAL
by FINSEQ_2:92, A41;
X2:
Sg . n is
Element of
(len (T . n)) -tuples_on REAL
by FINSEQ_2:92, A41;
B57:
((middle_sum Sf) . n) - ((middle_sum Sg) . n) =
(Sum (Sf . n)) - ((middle_sum Sg) . n)
by Def4
.=
(Sum (Sf . n)) - (Sum (Sg . n))
by Def4
.=
Sum (S . n)
by A57, X1, X2, RVSUM_1:90
.=
(middle_sum S) . n
by Def4
;
thus ((middle_sum Sf) . n) + ((- (middle_sum Sg)) . n) =
((middle_sum Sf) . n) + (- ((middle_sum Sg) . n))
by VALUED_1:8
.=
(middle_sum S) . n
by B57
;
verum end;
then
(middle_sum Sf) + (- (middle_sum Sg)) = middle_sum S
by SEQ_1:7;
hence
(middle_sum Sf) - (middle_sum Sg) = middle_sum S
by SEQ_1:11;
verum
end; hence
middle_sum S is
convergent
by A34, A35;
lim (middle_sum S) = (integral (u,rho1)) - (integral (u,rho2))thus
lim (middle_sum S) = (integral (u,rho1)) - (integral (u,rho2))
by A34, A35, A36, SEQ_2:12;
verum end;
hence
u is_RiemannStieltjes_integrable_with rho
; integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2))
hence
integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2))
by Def6, A3, A1; verum