let A be non empty closed_interval Subset of REAL; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2)) )
A3: now :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: 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 ; :: thesis: S2[i,x]
thus S2[i,x] by A8, A9; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S3[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: 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; :: thesis: 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 :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 :: thesis: for k being Element of NAT holds Sf . k is middle_volume of rho1,u,T . k
let k be Element of NAT ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S4[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: 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; :: thesis: 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 :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 :: thesis: for k being Element of NAT holds Sg . k is middle_volume of rho2,u,T . k
let k be Element of NAT ; :: thesis: 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 ; :: thesis: 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 :: thesis: for n being Nat holds ((middle_sum Sf) . n) + ((- (middle_sum Sg)) . n) = (middle_sum S) . n
let n be Nat; :: thesis: ((middle_sum Sf) . n) + ((- (middle_sum Sg)) . n) = (middle_sum S) . n
A37: 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 :: thesis: for j being object st j in dom (S . n) holds
(S . n) . j = ((Sf . n) . j) - ((Sg . n) . j)
let j be object ; :: thesis: ( j in dom (S . n) implies (S . n) . j = ((Sf . n) . j) - ((Sg . n) . j) )
assume A43: j in dom (S . n) ; :: thesis: (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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
hence middle_sum S is convergent by A34, A35; :: thesis: 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; :: thesis: verum
end;
hence u is_RiemannStieltjes_integrable_with rho ; :: thesis: integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2))
hence integral (u,rho) = (integral (u,rho1)) - (integral (u,rho2)) by Def6, A3, A1; :: thesis: verum