:: by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama

::

:: Received June 30, 2016

:: Copyright (c) 2016-2017 Association of Mizar Users

definition

let A be Subset of REAL;

let rho be real-valued Function;

coherence

( ( A is empty implies 0 is Real ) & ( not A is empty implies (rho . (upper_bound A)) - (rho . (lower_bound A)) is Real ) );

consistency

for b_{1} being Real holds verum;

;

end;
let rho be real-valued Function;

func vol (A,rho) -> Real equals :Defvol: :: INTEGR22:def 1

0 if A is empty

otherwise (rho . (upper_bound A)) - (rho . (lower_bound A));

correctness 0 if A is empty

otherwise (rho . (upper_bound A)) - (rho . (lower_bound A));

coherence

( ( A is empty implies 0 is Real ) & ( not A is empty implies (rho . (upper_bound A)) - (rho . (lower_bound A)) is Real ) );

consistency

for b

;

:: deftheorem Defvol defines vol INTEGR22:def 1 :

for A being Subset of REAL

for rho being real-valued Function holds

( ( A is empty implies vol (A,rho) = 0 ) & ( not A is empty implies vol (A,rho) = (rho . (upper_bound A)) - (rho . (lower_bound A)) ) );

for A being Subset of REAL

for rho being real-valued Function holds

( ( A is empty implies vol (A,rho) = 0 ) & ( not A is empty implies vol (A,rho) = (rho . (upper_bound A)) - (rho . (lower_bound A)) ) );

LmINTEGR208: for rho being real-valued Function

for A being non empty closed_interval Subset of REAL

for D being Division of A

for B being non empty closed_interval Subset of REAL

for v being FinSequence of REAL st A c= dom rho & B c= A & len D = len v & ( for i being Nat st i in dom v holds

v . i = vol ((B /\ (divset (D,i))),rho) ) holds

Sum v = vol (B,rho)

proof end;

theorem :: INTEGR22:1

for A being non empty closed_interval Subset of REAL

for D being Division of A

for rho being Function of A,REAL

for B being non empty closed_interval Subset of REAL

for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds

v . i = vol ((B /\ (divset (D,i))),rho) ) holds

Sum v = vol (B,rho)

for D being Division of A

for rho being Function of A,REAL

for B being non empty closed_interval Subset of REAL

for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds

v . i = vol ((B /\ (divset (D,i))),rho) ) holds

Sum v = vol (B,rho)

proof end;

theorem :: INTEGR22:2

for n, m being Nat

for a being Function of [:(Seg n),(Seg m):],REAL

for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds

ex r being FinSequence of REAL st

( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . (i,j) ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds

ex s being FinSequence of REAL st

( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . (i,j) ) ) ) holds

Sum p = Sum q

for a being Function of [:(Seg n),(Seg m):],REAL

for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds

ex r being FinSequence of REAL st

( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . (i,j) ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds

ex s being FinSequence of REAL st

( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . (i,j) ) ) ) holds

Sum p = Sum q

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let rho be real-valued Function;

let t be Division of A;

existence

ex b_{1} being FinSequence of REAL st

( len b_{1} = len t & ( for k being Nat st k in dom t holds

b_{1} . k = |.(vol ((divset (t,k)),rho)).| ) );

end;
let rho be real-valued Function;

let t be Division of A;

mode var_volume of rho,t -> FinSequence of REAL means :defvm: :: INTEGR22:def 2

( len it = len t & ( for k being Nat st k in dom t holds

it . k = |.(vol ((divset (t,k)),rho)).| ) );

correctness ( len it = len t & ( for k being Nat st k in dom t holds

it . k = |.(vol ((divset (t,k)),rho)).| ) );

existence

ex b

( len b

b

proof end;

:: deftheorem defvm defines var_volume INTEGR22:def 2 :

for A being non empty closed_interval Subset of REAL

for rho being real-valued Function

for t being Division of A

for b_{4} being FinSequence of REAL holds

( b_{4} is var_volume of rho,t iff ( len b_{4} = len t & ( for k being Nat st k in dom t holds

b_{4} . k = |.(vol ((divset (t,k)),rho)).| ) ) );

for A being non empty closed_interval Subset of REAL

for rho being real-valued Function

for t being Division of A

for b

( b

b

theorem LM1: :: INTEGR22:3

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for t being Division of A

for F being var_volume of rho,t

for k being Nat st k in dom F holds

0 <= F . k

for rho being Function of A,REAL

for t being Division of A

for F being var_volume of rho,t

for k being Nat st k in dom F holds

0 <= F . k

proof end;

theorem LM2: :: INTEGR22:4

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for t being Division of A

for F being var_volume of rho,t holds 0 <= Sum F

for rho being Function of A,REAL

for t being Division of A

for F being var_volume of rho,t holds 0 <= Sum F

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

end;
let rho be Function of A,REAL;

attr rho is bounded_variation means :: INTEGR22:def 3

ex d being Real st

( 0 < d & ( for t being Division of A

for F being var_volume of rho,t holds Sum F <= d ) );

ex d being Real st

( 0 < d & ( for t being Division of A

for F being var_volume of rho,t holds Sum F <= d ) );

:: deftheorem defines bounded_variation INTEGR22:def 3 :

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL holds

( rho is bounded_variation iff ex d being Real st

( 0 < d & ( for t being Division of A

for F being var_volume of rho,t holds Sum F <= d ) ) );

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL holds

( rho is bounded_variation iff ex d being Real st

( 0 < d & ( for t being Division of A

for F being var_volume of rho,t holds Sum F <= d ) ) );

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

assume AS: rho is bounded_variation ;

ex b_{1} being Real ex VD being non empty Subset of REAL st

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b_{1} = upper_bound VD )

for b_{1}, b_{2} being Real st ex VD being non empty Subset of REAL st

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b_{1} = upper_bound VD ) & ex VD being non empty Subset of REAL st

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b_{2} = upper_bound VD ) holds

b_{1} = b_{2}
;

end;
let rho be Function of A,REAL;

assume AS: rho is bounded_variation ;

func total_vd rho -> Real means :DeftotalVD: :: INTEGR22:def 4

ex VD being non empty Subset of REAL st

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & it = upper_bound VD );

existence ex VD being non empty Subset of REAL st

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & it = upper_bound VD );

ex b

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b

proof end;

uniqueness for b

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b

b

:: deftheorem DeftotalVD defines total_vd INTEGR22:def 4 :

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL st rho is bounded_variation holds

for b_{3} being Real holds

( b_{3} = total_vd rho iff ex VD being non empty Subset of REAL st

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b_{3} = upper_bound VD ) );

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL st rho is bounded_variation holds

for b

( b

( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b

theorem :: INTEGR22:5

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for T being Division of A st rho is bounded_variation holds

for F being var_volume of rho,T holds Sum F <= total_vd rho

for rho being Function of A,REAL

for T being Division of A st rho is bounded_variation holds

for F being var_volume of rho,T holds Sum F <= total_vd rho

proof end;

theorem :: INTEGR22:6

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL st rho is bounded_variation holds

0 <= total_vd rho

for rho being Function of A,REAL st rho is bounded_variation holds

0 <= total_vd rho

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

assume AS: ( rho is bounded_variation & dom u = A ) ;

let t be Division of A;

existence

ex b_{1} being FinSequence of REAL st

( len b_{1} = len t & ( for k being Nat st k in dom t holds

ex r being Real st

( r in rng (u | (divset (t,k))) & b_{1} . k = r * (vol ((divset (t,k)),rho)) ) ) );

end;
let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

assume AS: ( rho is bounded_variation & dom u = A ) ;

let t be Division of A;

mode middle_volume of rho,u,t -> FinSequence of REAL means :Def1: :: INTEGR22:def 5

( len it = len t & ( for k being Nat st k in dom t holds

ex r being Real st

( r in rng (u | (divset (t,k))) & it . k = r * (vol ((divset (t,k)),rho)) ) ) );

correctness ( len it = len t & ( for k being Nat st k in dom t holds

ex r being Real st

( r in rng (u | (divset (t,k))) & it . k = r * (vol ((divset (t,k)),rho)) ) ) );

existence

ex b

( len b

ex r being Real st

( r in rng (u | (divset (t,k))) & b

proof end;

:: deftheorem Def1 defines middle_volume INTEGR22:def 5 :

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

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

for t being Division of A

for b_{5} being FinSequence of REAL holds

( b_{5} is middle_volume of rho,u,t iff ( len b_{5} = len t & ( for k being Nat st k in dom t holds

ex r being Real st

( r in rng (u | (divset (t,k))) & b_{5} . k = r * (vol ((divset (t,k)),rho)) ) ) ) );

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

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

for t being Division of A

for b

( b

ex r being Real st

( r in rng (u | (divset (t,k))) & b

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

let T be DivSequence of A;

existence

ex b_{1} being sequence of (REAL *) st

for k being Element of NAT holds b_{1} . k is middle_volume of rho,u,T . k;

end;
let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

let T be DivSequence of A;

mode middle_volume_Sequence of rho,u,T -> sequence of (REAL *) means :Def3: :: INTEGR22:def 6

for k being Element of NAT holds it . k is middle_volume of rho,u,T . k;

correctness for k being Element of NAT holds it . k is middle_volume of rho,u,T . k;

existence

ex b

for k being Element of NAT holds b

proof end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR22:def 6 :

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL

for T being DivSequence of A

for b_{5} being sequence of (REAL *) holds

( b_{5} is middle_volume_Sequence of rho,u,T iff for k being Element of NAT holds b_{5} . k is middle_volume of rho,u,T . k );

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL

for T being DivSequence of A

for b

( b

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of rho,u,T;

let k be Nat;

:: original: .

redefine func S . k -> middle_volume of rho,u,T . k;

coherence

S . k is middle_volume of rho,u,T . k

end;
let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of rho,u,T;

let k be Nat;

:: original: .

redefine func S . k -> middle_volume of rho,u,T . k;

coherence

S . k is middle_volume of rho,u,T . k

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of rho,u,T;

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = Sum (S . i)

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = Sum (S . i) ) & ( for i being Nat holds b_{2} . i = Sum (S . i) ) holds

b_{1} = b_{2}

end;
let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of rho,u,T;

func middle_sum S -> Real_Sequence means :Def4: :: INTEGR22:def 7

for i being Nat holds it . i = Sum (S . i);

existence for i being Nat holds it . i = Sum (S . i);

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines middle_sum INTEGR22:def 7 :

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T

for b_{6} being Real_Sequence holds

( b_{6} = middle_sum S iff for i being Nat holds b_{6} . i = Sum (S . i) );

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T

for b

( b

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

end;
let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

pred u is_RiemannStieltjes_integrable_with rho means :: INTEGR22:def 8

ex I being Real st

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) = I );

ex I being Real st

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) = I );

:: deftheorem defines is_RiemannStieltjes_integrable_with INTEGR22:def 8 :

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL holds

( u is_RiemannStieltjes_integrable_with rho iff ex I being Real st

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) = I ) );

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL holds

( u is_RiemannStieltjes_integrable_with rho iff ex I being Real st

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) = I ) );

definition

let A be non empty closed_interval Subset of REAL;

let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

assume A1: ( rho is bounded_variation & dom u = A & u is_RiemannStieltjes_integrable_with rho ) ;

ex b_{1} being Real st

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) = b_{1} )
by A1;

uniqueness

for b_{1}, b_{2} being Real st ( 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) = b_{1} ) ) & ( 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) = b_{2} ) ) holds

b_{1} = b_{2}

end;
let rho be Function of A,REAL;

let u be PartFunc of REAL,REAL;

assume A1: ( rho is bounded_variation & dom u = A & u is_RiemannStieltjes_integrable_with rho ) ;

func integral (u,rho) -> Real means :Def6: :: INTEGR22:def 9

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) = it );

existence 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) = it );

ex b

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) = b

uniqueness

for b

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) = b

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) = b

b

proof end;

:: deftheorem Def6 defines integral INTEGR22:def 9 :

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

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

for b_{4} being Real holds

( b_{4} = integral (u,rho) iff 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) = b_{4} ) );

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

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

for b

( b

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) = b

theorem Th4: :: INTEGR22:7

for A being non empty closed_interval Subset of REAL

for r being Real

for rho being Function of A,REAL

for u, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom w = A & w = r (#) u & u is_RiemannStieltjes_integrable_with rho holds

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = r * (integral (u,rho)) )

for r being Real

for rho being Function of A,REAL

for u, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom w = A & w = r (#) u & u is_RiemannStieltjes_integrable_with rho holds

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = r * (integral (u,rho)) )

proof end;

reconsider jj = 1 as Real ;

theorem Th5: :: INTEGR22:8

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

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

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = - (integral (u,rho)) )

for rho being Function of A,REAL

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

( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = - (integral (u,rho)) )

proof end;

theorem Th6: :: INTEGR22:9

for A being non empty closed_interval Subset of REAL

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

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

proof end;

theorem :: INTEGR22:10

for A being non empty closed_interval Subset of REAL

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

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

proof end;

theorem Lm4A: :: INTEGR22:11

for A, B being non empty closed_interval Subset of REAL

for r being Real

for rho, rho1 being Function of A,REAL st B c= A & rho = r (#) rho1 holds

vol (B,rho) = r * (vol (B,rho1))

for r being Real

for rho, rho1 being Function of A,REAL st B c= A & rho = r (#) rho1 holds

vol (B,rho) = r * (vol (B,rho1))

proof end;

theorem Th4A: :: INTEGR22:12

for A being non empty closed_interval Subset of REAL

for r being Real

for rho, rho1 being Function of A,REAL

for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = r (#) rho1 & u is_RiemannStieltjes_integrable_with rho1 holds

( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = r * (integral (u,rho1)) )

for r being Real

for rho, rho1 being Function of A,REAL

for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = r (#) rho1 & u is_RiemannStieltjes_integrable_with rho1 holds

( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = r * (integral (u,rho1)) )

proof end;

theorem :: INTEGR22:13

for A being non empty closed_interval Subset of REAL

for rho, rho1 being Function of A,REAL

for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = - rho1 & u is_RiemannStieltjes_integrable_with rho1 holds

( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = - (integral (u,rho1)) )

for rho, rho1 being Function of A,REAL

for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = - rho1 & u is_RiemannStieltjes_integrable_with rho1 holds

( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = - (integral (u,rho1)) )

proof end;

theorem Lm6A: :: INTEGR22:14

for A, B being non empty closed_interval Subset of REAL

for rho, rho1, rho2 being Function of A,REAL st B c= A & rho = rho1 + rho2 holds

vol (B,rho) = (vol (B,rho1)) + (vol (B,rho2))

for rho, rho1, rho2 being Function of A,REAL st B c= A & rho = rho1 + rho2 holds

vol (B,rho) = (vol (B,rho1)) + (vol (B,rho2))

proof end;

theorem :: INTEGR22:15

for A being 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)) )

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

proof end;

theorem Lm7A: :: INTEGR22:16

for A, B being non empty closed_interval Subset of REAL

for rho, rho1, rho2 being Function of A,REAL st B c= A & rho = rho1 - rho2 holds

vol (B,rho) = (vol (B,rho1)) - (vol (B,rho2))

for rho, rho1, rho2 being Function of A,REAL st B c= A & rho = rho1 - rho2 holds

vol (B,rho) = (vol (B,rho1)) - (vol (B,rho2))

proof end;

theorem :: INTEGR22:17

for A being 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)) )

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

proof end;