let A be non empty closed_interval Subset of REAL; :: thesis:
let rho be Function of A,REAL; :: thesis:
let f be Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))); :: thesis:
assume that
A1: rho is bounded_variation and
A2: for u being continuous PartFunc of REAL,REAL st dom u = A holds
f . u = integral (u,rho) ; :: thesis:
set X = R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A);
A3: for u being continuous PartFunc of REAL,REAL st u in the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) holds
f . u = integral (u,rho)

proof

let u be continuous PartFunc of REAL,REAL; :: thesis:
assume u in the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) ; :: thesis:
then ( dom u = A & u is continuous PartFunc of REAL,REAL ) by Th80;
hence f . u = integral (u,rho) by A2; :: thesis:

end;

A4: for u being continuous PartFunc of REAL,REAL
for v being Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) st dom u = A & u = v holds
|.(integral (u,rho)).| <= ||.v.|| * (total_vd rho)

proof

let u be continuous PartFunc of REAL,REAL; :: thesis:
let v be Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)); :: thesis:
assume A5: ( dom u = A & u = v ) ; :: thesis:
then B6: u is_RiemannStieltjes_integrable_with rho by A1, INTEGR23:21;
consider T being DivSequence of A such that
A7: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;
set S = the middle_volume_Sequence of rho,u,T;
A9: |.(middle_sum the middle_volume_Sequence of rho,u,T).| is convergent by SEQ_4:13, B6, A7;
A10: for n being Nat holds |.((middle_sum the middle_volume_Sequence of rho,u,T) . n).| <= ||.v.|| * (total_vd rho)

proof

let n be Nat; :: thesis:
set F = the var_volume of rho,T . n;
reconsider v0 = ||.v.|| as Real ;
reconsider vF = v0 * the var_volume of rho,T . n as FinSequence of REAL ;
dom the var_volume of rho,T . n = Seg (len the var_volume of rho,T . n) by FINSEQ_1:def 3;
then B14: dom vF = Seg (len the var_volume of rho,T . n) by VALUED_1:def 5;
A15: len ( the middle_volume_Sequence of rho,u,T . n) = len (T . n) by A1, A5, INTEGR22:def 5
.= len the var_volume of rho,T . n by INTEGR22:def 2
.= len vF by B14, FINSEQ_1:def 3 ;
for j being Nat st j in dom ( the middle_volume_Sequence of rho,u,T . n) holds
|.(( the middle_volume_Sequence of rho,u,T . n) . j).| <= vF . j

proof

let j be Nat; :: thesis:
assume j in dom ( the middle_volume_Sequence of rho,u,T . n) ; :: thesis:
then B17: j in Seg (len ( the middle_volume_Sequence of rho,u,T . n)) by FINSEQ_1:def 3;
then j in Seg (len (T . n)) by A1, A5, INTEGR22:def 5;
then A16: j in dom (T . n) by FINSEQ_1:def 3;
consider r being Real such that
A18: r in rng (u | (divset ((T . n),j))) and
A19: ( the middle_volume_Sequence of rho,u,T . n) . j = r * (vol ((divset ((T . n),j)),rho)) by A1, A5, INTEGR22:def 5, A16;
A20: |.(( the middle_volume_Sequence of rho,u,T . n) . j).| = |.r.| * |.(vol ((divset ((T . n),j)),rho)).| by COMPLEX1:65, A19
.= |.r.| * ( the var_volume of rho,T . n . j) by A16, INTEGR22:def 2 ;
consider x being object such that
A21: ( x in dom (u | (divset ((T . n),j))) & r = (u | (divset ((T . n),j))) . x ) by A18, FUNCT_1:def 3;
set AV = the carrier of (ClstoCmp A);
u in BoundedFunctions the carrier of (ClstoCmp A) by A5, Lm2;
then consider u1 being Function of the carrier of (ClstoCmp A),REAL such that
A23: ( u = u1 & u1 | the carrier of (ClstoCmp A) is bounded ) ;
x in A by A5, A21, RELAT_1:57;
then reconsider x1 = x as Element of the carrier of (ClstoCmp A) by Lm1;
reconsider v1 = v as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by Lm2;
|.(u1 . x1).| <= ||.v1.|| by A5, A23, C0SP1:26;
then |.(u . x).| <= ||.v.|| by A23, FUNCT_1:49;
then A24: |.r.| <= ||.v.|| by A21, FUNCT_1:47;
j in Seg (len (T . n)) by B17, A1, A5, INTEGR22:def 5;
then j in Seg (len the var_volume of rho,T . n) by INTEGR22:def 2;
then j in dom the var_volume of rho,T . n by FINSEQ_1:def 3;
then 0 <= the var_volume of rho,T . n . j by INTEGR22:3;
then |.r.| * ( the var_volume of rho,T . n . j) <= v0 * ( the var_volume of rho,T . n . j) by A24, XREAL_1:64;
hence |.(( the middle_volume_Sequence of rho,u,T . n) . j).| <= vF . j by A20, VALUED_1:6; :: thesis:

end;

then |.(Sum ( the middle_volume_Sequence of rho,u,T . n)).| <= Sum vF by A15, INTEGR23:3;
then A25: |.(Sum ( the middle_volume_Sequence of rho,u,T . n)).| <= ||.v.|| * (Sum the var_volume of rho,T . n) by RVSUM_1:87;
||.v.|| * (Sum the var_volume of rho,T . n) <= ||.v.|| * (total_vd rho) by A1, INTEGR22:5, XREAL_1:64;
then |.(Sum ( the middle_volume_Sequence of rho,u,T . n)).| <= ||.v.|| * (total_vd rho) by A25, XXREAL_0:2;
hence |.((middle_sum the middle_volume_Sequence of rho,u,T) . n).| <= ||.v.|| * (total_vd rho) by INTEGR22:def 7; :: thesis:

end;

reconsider a = ||.v.|| * (total_vd rho) as Real ;

now :: thesis:

end;

then lim |.(middle_sum the middle_volume_Sequence of rho,u,T).| <= lim (seq_const a) by A9, SEQ_2:18;
then A27: |.(lim (middle_sum the middle_volume_Sequence of rho,u,T)).| <= lim (seq_const a) by B6, A7, SEQ_4:14;
lim (seq_const a) = (seq_const a) . 0 by SEQ_4:26
.= a by SEQ_1:57 ;
hence |.(integral (u,rho)).| <= ||.v.|| * (total_vd rho) by B6, A1, A5, INTEGR22:def 9, A7, A27; :: thesis:

end;

reconsider g = f as Lipschitzian linear-Functional of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) by DUALSP01:def 10;

now :: thesis:

let k be Real; :: thesis:
assume k in PreNorms g ; :: thesis:
then consider u being Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) such that
A28: ( k = |.(g . u).| & ||.u.|| <= 1 ) ;
u in ContinuousFunctions (ClstoCmp A) ;
then ex v being continuous RealMap of (ClstoCmp A) st u = v ;
then reconsider v = u as Function ;
A29: ( dom v = A & v is continuous PartFunc of REAL,REAL ) by Th80;
reconsider v = v as continuous PartFunc of REAL,REAL by Th80;
|.(integral (v,rho)).| <= ||.u.|| * (total_vd rho) by A4, A29;
then A30: |.(g . u).| <= ||.u.|| * (total_vd rho) by A3;
0 <= total_vd rho by A1, INTEGR22:6;
then ||.u.|| * (total_vd rho) <= 1 * (total_vd rho) by A28, XREAL_1:64;
hence k <= total_vd rho by A28, A30, XXREAL_0:2; :: thesis:

end;

then upper_bound (PreNorms g) <= total_vd rho by SEQ_4:45;
hence ||.f.|| <= total_vd rho by DUALSP01:24; :: thesis: