let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL

for u, v, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho holds

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) )

let rho be Function of A,REAL; :: thesis: for u, v, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho holds

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) )

let u, v, w be PartFunc of REAL,REAL; :: thesis: ( rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho implies ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) ) )

assume A1: ( rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho ) ; :: thesis: ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) )

hence integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) by Def6, A3, A1; :: thesis: verum

for u, v, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho holds

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) )

let rho be Function of A,REAL; :: thesis: for u, v, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho holds

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) )

let u, v, w be PartFunc of REAL,REAL; :: thesis: ( rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho implies ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) ) )

assume A1: ( rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u + v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho ) ; :: thesis: ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) )

A3: now :: thesis: for T being DivSequence of A

for S being middle_volume_Sequence of rho,w,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) )

hence
w is_RiemannStieltjes_integrable_with rho
; :: thesis: integral (w,rho) = (integral (u,rho)) + (integral (v,rho))for S being middle_volume_Sequence of rho,w,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) )

let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of rho,w,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) )

let S be middle_volume_Sequence of rho,w,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) ) )

assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) )

defpred S_{1}[ 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 (w | (divset ((T . $1),i))) & ex z being Real st

( z = (w | (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 S_{1}[k,p]

A11: for x being Element of NAT holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A5);

defpred S_{2}[ Element of NAT , set ] means ex q being middle_volume of rho,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)),rho)) ) ) );

A12: for k being Element of NAT ex y being Element of REAL * st S_{2}[k,y]

A22: for x being Element of NAT holds S_{2}[x,Sf . x]
from FUNCT_2:sch 3(A12);

defpred S_{3}[ Element of NAT , set ] means ex q being middle_volume of rho,v,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 (v | (divset ((T . $1),i))) & z = (v | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = z * (vol ((divset ((T . $1),i)),rho)) ) ) );

A23: for k being Element of NAT ex y being Element of REAL * st S_{3}[k,y]

A33: for x being Element of NAT holds S_{3}[x,Sg . x]
from FUNCT_2:sch 3(A23);

A34: ( middle_sum Sf is convergent & lim (middle_sum Sf) = integral (u,rho) ) by A1, A4, Def6;

A35: ( middle_sum Sg is convergent & lim (middle_sum Sg) = integral (v,rho) ) by A1, A4, Def6;

A36: (middle_sum Sf) + (middle_sum Sg) = middle_sum S

thus lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) by A34, A35, A36, SEQ_2:6; :: thesis: verum

end;( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) )

let S be middle_volume_Sequence of rho,w,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) ) )

assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum S is convergent & lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) )

defpred S

( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds

( p . i in dom (w | (divset ((T . $1),i))) & ex z being Real st

( z = (w | (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 S

proof

consider F being sequence of (REAL *) such that
let k be Element of NAT ; :: thesis: ex p being Element of REAL * st S_{1}[k,p]

defpred S_{2}[ Nat, set ] means ( $2 in dom (w | (divset ((T . k),$1))) & ex c being Real st

( c = (w | (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 S_{2}[i,x]

A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S_{2}[i,p . i] ) )
from FINSEQ_1:sch 5(A7);

take p ; :: thesis: ( p is Element of REAL * & S_{1}[k,p] )

len p = len (T . k) by A10, FINSEQ_1:def 3;

hence ( p is Element of REAL * & S_{1}[k,p] )
by A10, A6, FINSEQ_1:def 11; :: thesis: verum

end;defpred S

( c = (w | (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 S

proof

consider p being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S_{2}[i,x] )

assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S_{2}[i,x]

then i in dom (T . k) by FINSEQ_1:def 3;

then consider c being Real such that

A8: ( c in rng (w | (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 (w | (divset ((T . k),i))) & c = (w | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def 3;

reconsider x = x as Element of REAL by A9;

take x ; :: thesis: S_{2}[i,x]

thus S_{2}[i,x]
by A8, A9; :: thesis: verum

end;assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S

then i in dom (T . k) by FINSEQ_1:def 3;

then consider c being Real such that

A8: ( c in rng (w | (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 (w | (divset ((T . k),i))) & c = (w | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def 3;

reconsider x = x as Element of REAL by A9;

take x ; :: thesis: S

thus S

A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S

take p ; :: thesis: ( p is Element of REAL * & S

len p = len (T . k) by A10, FINSEQ_1:def 3;

hence ( p is Element of REAL * & S

A11: for x being Element of NAT holds S

defpred S

( 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)),rho)) ) ) );

A12: for k being Element of NAT ex y being Element of REAL * st S

proof

consider Sf being sequence of (REAL *) such that
let k be Element of NAT ; :: thesis: ex y being Element of REAL * st S_{2}[k,y]

defpred S_{3}[ 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)),rho)) );

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 S_{3}[i,x]

A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S_{3}[i,q . i] ) )
from FINSEQ_1:sch 5(A14);

A20: len q = len (T . k) by A19, FINSEQ_1:def 3;

q is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S_{2}[k,y]
by A13, A19; :: thesis: verum

end;defpred S

( (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)),rho)) );

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 S

proof

consider q being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S_{3}[i,x] )

assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S_{3}[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 (w | (divset ((T . k),i))) & ex z being Real st

( z = (w | (divset ((T . k),i))) . (p . i) & (S . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) ) by A11;

p . i in dom (w | (divset ((T . k),i))) by A15, A16;

then A17: ( p . i in dom w & p . i in divset ((T . k),i) ) by RELAT_1:57;

then p . i in dom (u | (divset ((T . k),i))) by A1, RELAT_1:57;

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)),rho)) is Element of REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S_{3}[i,x]
by A16, A17, A1, RELAT_1:57; :: thesis: verum

end;assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S

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 (w | (divset ((T . k),i))) & ex z being Real st

( z = (w | (divset ((T . k),i))) . (p . i) & (S . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) ) by A11;

p . i in dom (w | (divset ((T . k),i))) by A15, A16;

then A17: ( p . i in dom w & p . i in divset ((T . k),i) ) by RELAT_1:57;

then p . i in dom (u | (divset ((T . k),i))) by A1, RELAT_1:57;

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)),rho)) is Element of REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S

A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S

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)),rho)) )

then reconsider q = q as middle_volume of rho,u,T . k by A20, Def1, A1;ex c being Real st

( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) )

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)),rho)) ) )

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)),rho)) )

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)),rho)) ) by A19;

thus ex c being Real st

( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) by A21, FUNCT_1:3; :: thesis: verum

end;( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) )

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)),rho)) )

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)),rho)) ) by A19;

thus ex c being Real st

( c in rng (u | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) by A21, FUNCT_1:3; :: thesis: verum

q is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S

A22: for x being Element of NAT holds S

now :: thesis: for k being Element of NAT holds Sf . k is middle_volume of rho,u,T . k

then reconsider Sf = Sf as middle_volume_Sequence of rho,u,T by Def3;let k be Element of NAT ; :: thesis: Sf . k is middle_volume of rho,u,T . k

ex q being middle_volume of rho,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)),rho)) ) ) ) by A22;

hence Sf . k is middle_volume of rho,u,T . k ; :: thesis: verum

end;ex q being middle_volume of rho,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)),rho)) ) ) ) by A22;

hence Sf . k is middle_volume of rho,u,T . k ; :: thesis: verum

defpred S

( q = $2 & ( for i being Nat st i in dom (T . $1) holds

ex z being Real st

( (F . $1) . i in dom (v | (divset ((T . $1),i))) & z = (v | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = z * (vol ((divset ((T . $1),i)),rho)) ) ) );

A23: for k being Element of NAT ex y being Element of REAL * st S

proof

consider Sg being sequence of (REAL *) such that
let k be Element of NAT ; :: thesis: ex y being Element of REAL * st S_{3}[k,y]

defpred S_{4}[ Nat, set ] means ex c being Real st

( (F . k) . $1 in dom (v | (divset ((T . k),$1))) & c = (v | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = c * (vol ((divset ((T . k),$1)),rho)) );

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 S_{4}[i,x]

A30: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S_{4}[i,q . i] ) )
from FINSEQ_1:sch 5(A25);

A31: len q = len (T . k) by A30, FINSEQ_1:def 3;

q is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S_{3}[k,y]
by A24, A30; :: thesis: verum

end;defpred S

( (F . k) . $1 in dom (v | (divset ((T . k),$1))) & c = (v | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = c * (vol ((divset ((T . k),$1)),rho)) );

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 S

proof

consider q being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S_{4}[i,x] )

assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S_{4}[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 (w | (divset ((T . k),i))) & ex z being Real st

( z = (w | (divset ((T . k),i))) . (p . i) & (S . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) ) by A11;

p . i in dom (w | (divset ((T . k),i))) by A26, A27;

then A28: ( p . i in dom w & p . i in divset ((T . k),i) ) by RELAT_1:57;

then p . i in dom (v | (divset ((T . k),i))) by A1, RELAT_1:57;

then (v | (divset ((T . k),i))) . (p . i) in rng (v | (divset ((T . k),i))) by FUNCT_1:3;

then reconsider x = (v | (divset ((T . k),i))) . (p . i) as Element of REAL ;

x * (vol ((divset ((T . k),i)),rho)) is Element of REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S_{4}[i,x]
by A27, A28, A1, RELAT_1:57; :: thesis: verum

end;assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S

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 (w | (divset ((T . k),i))) & ex z being Real st

( z = (w | (divset ((T . k),i))) . (p . i) & (S . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) ) by A11;

p . i in dom (w | (divset ((T . k),i))) by A26, A27;

then A28: ( p . i in dom w & p . i in divset ((T . k),i) ) by RELAT_1:57;

then p . i in dom (v | (divset ((T . k),i))) by A1, RELAT_1:57;

then (v | (divset ((T . k),i))) . (p . i) in rng (v | (divset ((T . k),i))) by FUNCT_1:3;

then reconsider x = (v | (divset ((T . k),i))) . (p . i) as Element of REAL ;

x * (vol ((divset ((T . k),i)),rho)) is Element of REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S

A30: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S

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 (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) )

then reconsider q = q as middle_volume of rho,v,T . k by A31, Def1, A1;ex c being Real st

( c in rng (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) )

let i be Nat; :: thesis: ( i in dom (T . k) implies ex c being Real st

( c in rng (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) )

assume i in dom (T . k) ; :: thesis: ex c being Real st

( c in rng (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) )

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 (v | (divset ((T . k),i))) & c = (v | (divset ((T . k),i))) . ((F . k) . i) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) by A30;

thus ex c being Real st

( c in rng (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) by A32, FUNCT_1:3; :: thesis: verum

end;( c in rng (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) )

assume i in dom (T . k) ; :: thesis: ex c being Real st

( c in rng (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) )

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 (v | (divset ((T . k),i))) & c = (v | (divset ((T . k),i))) . ((F . k) . i) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) by A30;

thus ex c being Real st

( c in rng (v | (divset ((T . k),i))) & q . i = c * (vol ((divset ((T . k),i)),rho)) ) by A32, FUNCT_1:3; :: thesis: verum

q is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S

A33: for x being Element of NAT holds S

now :: thesis: for k being Element of NAT holds Sg . k is middle_volume of rho,v,T . k

then reconsider Sg = Sg as middle_volume_Sequence of rho,v,T by Def3;let k be Element of NAT ; :: thesis: Sg . k is middle_volume of rho,v,T . k

ex q being middle_volume of rho,v,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 (v | (divset ((T . k),i))) & z = (v | (divset ((T . k),i))) . ((F . k) . i) & q . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) by A33;

hence Sg . k is middle_volume of rho,v,T . k ; :: thesis: verum

end;ex q being middle_volume of rho,v,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 (v | (divset ((T . k),i))) & z = (v | (divset ((T . k),i))) . ((F . k) . i) & q . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) by A33;

hence Sg . k is middle_volume of rho,v,T . k ; :: thesis: verum

A34: ( middle_sum Sf is convergent & lim (middle_sum Sf) = integral (u,rho) ) by A1, A4, Def6;

A35: ( middle_sum Sg is convergent & lim (middle_sum Sg) = integral (v,rho) ) by A1, A4, Def6;

A36: (middle_sum Sf) + (middle_sum Sg) = middle_sum S

proof

end;

hence
middle_sum S is convergent
by A34, A35; :: thesis: lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho))now :: thesis: for n being Nat holds ((middle_sum Sf) . n) + ((middle_sum Sg) . n) = (middle_sum S) . n

hence
(middle_sum Sf) + (middle_sum Sg) = middle_sum S
by SEQ_1:7; :: thesis: verumlet 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 (w | (divset ((T . n),i))) & ex z being Real st

( z = (w | (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 rho,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)),rho)) ) ) ) by A22, A37;

consider r being middle_volume of rho,v,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 (v | (divset ((T . n),i))) & z = (v | (divset ((T . n),i))) . ((F . n) . i) & r . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) 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;

A42: ( dom (Sf . n) = dom (T . n) & dom (Sg . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by A41, FINSEQ_3:29;

B42: dom (S . n) = (dom (Sf . n)) /\ (dom (Sg . n)) by A42;

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;

thus ((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:89

.= (middle_sum S) . n by Def4 ; :: thesis: verum

end;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 (w | (divset ((T . n),i))) & ex z being Real st

( z = (w | (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 rho,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)),rho)) ) ) ) by A22, A37;

consider r being middle_volume of rho,v,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 (v | (divset ((T . n),i))) & z = (v | (divset ((T . n),i))) . ((F . n) . i) & r . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) 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;

A42: ( dom (Sf . n) = dom (T . n) & dom (Sg . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by A41, FINSEQ_3:29;

B42: dom (S . n) = (dom (Sf . n)) /\ (dom (Sg . n)) by A42;

now :: thesis: for j being object st j in dom (S . n) holds

(S . n) . j = ((Sf . n) . j) + ((Sg . n) . j)

then A57:
(Sf . n) + (Sg . n) = S . n
by B42, VALUED_1:def 1;(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 = (w | (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)),rho)) ) by A39, A43, A42;

consider w1 being Real such that

A46: ( (F . n) . i in dom (v | (divset ((T . n),i))) & w1 = (v | (divset ((T . n),i))) . ((F . n) . i) & r . i = w1 * (vol ((divset ((T . n),i)),rho)) ) by A40, A43, A42;

A47: (F . n) . i in divset ((T . n),i) by A46, RELAT_1:57;

A50: (F . n) . i in dom w by A1, A46, RELAT_1:57;

A53: v . ((F . n) . i) = w1 by A46, A47, FUNCT_1:49;

A54: t = w . ((F . n) . i) by A47, FUNCT_1:49, A44

.= (u . ((F . n) . i)) + (v . ((F . n) . i)) by A50, A1, VALUED_1:def 1

.= z + w1 by A45, A47, FUNCT_1:49, A53 ;

thus (S . n) . j = ((Sf . n) . j) + ((Sg . n) . j) by A45, A39, A46, A40, A54, A44; :: thesis: verum

end;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 = (w | (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)),rho)) ) by A39, A43, A42;

consider w1 being Real such that

A46: ( (F . n) . i in dom (v | (divset ((T . n),i))) & w1 = (v | (divset ((T . n),i))) . ((F . n) . i) & r . i = w1 * (vol ((divset ((T . n),i)),rho)) ) by A40, A43, A42;

A47: (F . n) . i in divset ((T . n),i) by A46, RELAT_1:57;

A50: (F . n) . i in dom w by A1, A46, RELAT_1:57;

A53: v . ((F . n) . i) = w1 by A46, A47, FUNCT_1:49;

A54: t = w . ((F . n) . i) by A47, FUNCT_1:49, A44

.= (u . ((F . n) . i)) + (v . ((F . n) . i)) by A50, A1, VALUED_1:def 1

.= z + w1 by A45, A47, FUNCT_1:49, A53 ;

thus (S . n) . j = ((Sf . n) . j) + ((Sg . n) . j) by A45, A39, A46, A40, A54, A44; :: thesis: verum

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;

thus ((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:89

.= (middle_sum S) . n by Def4 ; :: thesis: verum

thus lim (middle_sum S) = (integral (u,rho)) + (integral (v,rho)) by A34, A35, A36, SEQ_2:6; :: thesis: verum

hence integral (w,rho) = (integral (u,rho)) + (integral (v,rho)) by Def6, A3, A1; :: thesis: verum