let A be non empty closed_interval Subset of REAL; for rho being Function of A,REAL
for u being continuous PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds
u is_RiemannStieltjes_integrable_with rho
let rho be Function of A,REAL; for u being continuous PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds
u is_RiemannStieltjes_integrable_with rho
let u be continuous PartFunc of REAL,REAL; ( rho is bounded_variation & dom u = A implies u is_RiemannStieltjes_integrable_with rho )
assume A1:
( rho is bounded_variation & dom u = A )
; u is_RiemannStieltjes_integrable_with rho
A2:
u | A is uniformly_continuous
by A1, FCONT_2:11;
consider T0 being DivSequence of A such that
A3:
( delta T0 is convergent & lim (delta T0) = 0 )
by INTEGRA4:11;
set S0 = the middle_volume_Sequence of rho,u,T0;
set I = lim (middle_sum the middle_volume_Sequence of rho,u,T0);
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) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) )
proof
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) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) )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) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) ) )
assume A4:
(
delta T is
convergent &
lim (delta T) = 0 )
;
( middle_sum S is convergent & lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0) )
hence
middle_sum S is
convergent
by A1, A2, Th20;
lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0)
consider T1 being
DivSequence of
A such that A5:
for
i being
Nat holds
(
T1 . (2 * i) = T0 . i &
T1 . ((2 * i) + 1) = T . i )
by INTEGR20:15;
consider S1 being
middle_volume_Sequence of
rho,
u,
T1 such that A6:
for
i being
Nat holds
(
S1 . (2 * i) = the
middle_volume_Sequence of
rho,
u,
T0 . i &
S1 . ((2 * i) + 1) = S . i )
by A5, Th21;
(
delta T1 is
convergent &
lim (delta T1) = 0 )
by A3, A4, A5, INTEGR20:16;
then A7:
middle_sum S1 is
convergent
by A1, A2, Th20;
A8:
for
i being
Nat holds
(
(middle_sum S1) . (2 * i) = (middle_sum the middle_volume_Sequence of rho,u,T0) . i &
(middle_sum S1) . ((2 * i) + 1) = (middle_sum S) . i )
proof
let i be
Nat;
( (middle_sum S1) . (2 * i) = (middle_sum the middle_volume_Sequence of rho,u,T0) . i & (middle_sum S1) . ((2 * i) + 1) = (middle_sum S) . i )
reconsider S1 =
S1 as
middle_volume_Sequence of
rho,
u,
T1 ;
(
S1 . (2 * i) = the
middle_volume_Sequence of
rho,
u,
T0 . i &
T1 . (2 * i) = T0 . i &
S1 . ((2 * i) + 1) = S . i &
T1 . ((2 * i) + 1) = T . i )
by A5, A6;
then
(
(middle_sum S1) . (2 * i) = Sum ( the middle_volume_Sequence of rho,u,T0 . i) &
(middle_sum S1) . ((2 * i) + 1) = Sum (S . i) )
by INTEGR22:def 7;
hence
(
(middle_sum S1) . (2 * i) = (middle_sum the middle_volume_Sequence of rho,u,T0) . i &
(middle_sum S1) . ((2 * i) + 1) = (middle_sum S) . i )
by INTEGR22:def 7;
verum
end;
lim (middle_sum S) = lim (middle_sum S1)
by A7, A8, Th22;
hence
lim (middle_sum S) = lim (middle_sum the middle_volume_Sequence of rho,u,T0)
by A7, A8, Th22;
verum
end;
hence
u is_RiemannStieltjes_integrable_with rho
by INTEGR22:def 8; verum