let A be non empty closed_interval Subset of REAL; :: thesis: for x being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st 0 < vol A holds
ex rho being Function of A,REAL st
( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )
let x be Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))); :: thesis: ( 0 < vol A implies ex rho being Function of A,REAL st
( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho ) )
assume A1: 0 < vol A ; :: thesis: ex rho being Function of A,REAL st
( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )
set X = R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A);
set V = R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A);
set AV = the carrier of (ClstoCmp A);
A2: the carrier of (ClstoCmp A) = A by Lm1;
R_Algebra_of_ContinuousFunctions (ClstoCmp A) is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A) by C0SP2:9;
then A3: ( the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) c= the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) & the addF of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) = the addF of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) || the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) & the Mult of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) = the Mult of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) | [:REAL, the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)):] ) by C0SP1:def 9;
A4: 0. (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) = (ClstoCmp A) --> 0 by C0SP2:12
.= 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by C0SP1:25 ;
B5: R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A) is SubRealNormSpace of R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A) by A3, A4, DUALSP01:def 16;
reconsider h = x as Lipschitzian linear-Functional of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) by DUALSP01:def 10;
consider f being Lipschitzian linear-Functional of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)), F being Point of (DualSp (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))) such that
A6: ( f = F & f | the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) = h & ||.F.|| = ||.x.|| ) by B5, DUALSP01:36;
consider a, b being Real such that
A7: ( a <= b & [.a,b.] = A & ClstoCmp A = Closed-Interval-TSpace (a,b) ) by Def7ClstoCmp;
consider m being Function of A,(BoundedFunctions A) such that
A8: for s being Real st s in [.a,b.] holds
( ( s = a implies m . s = [.a,b.] --> 0 ) & ( s <> a implies m . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) ) by A7, LM83;
the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) = BoundedFunctions A by Lm1;
then reconsider rho = f * m as Function of A,REAL ;
A9: for D being Division of A
for K being var_volume of rho,D st a < D . 1 holds
Sum K <= ||.x.||

proof

let D be Division of A; :: thesis: for K being var_volume of rho,D st a < D . 1 holds
Sum K <= ||.x.||
let K be var_volume of rho,D; :: thesis: ( a < D . 1 implies Sum K <= ||.x.|| )
assume A10: a < D . 1 ; :: thesis: Sum K <= ||.x.||
consider s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that
A11: len s = len D and
A12: for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) by LM84;
set yD = Sum s;
Sum s in the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
then Sum s in BoundedFunctions A by Lm1;
then consider g being Function of A,REAL such that
A13: ( g = Sum s & g | A is bounded ) ;
A14: f . (Sum s) = Sum (f * s) by LM87;
A15: for t being Element of A holds |.(g . t).| <= 1

proof

let t be Element of A; :: thesis: |.(g . t).| <= 1
defpred S₁[ Nat, set ] means ex sk being Function of A,REAL st
( sk = s . $1 & $2 = sk . t );
A16: for k being Nat st k in Seg (len D) holds
ex x being Element of REAL st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of REAL st S₁[k,x] )
assume k in Seg (len D) ; :: thesis: ex x being Element of REAL st S₁[k,x]
then k in dom s by FINSEQ_1:def 3, A11;
then s . k = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k))) by A12;
then s . k in the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
then s . k in BoundedFunctions A by Lm1;
then consider sk being Function of A,REAL such that
A17: ( sk = s . k & sk | A is bounded ) ;
take x = sk . t; :: thesis: S₁[k,x]
thus S₁[k,x] by A17; :: thesis: verum

end;

consider z being FinSequence of REAL such that
A18: ( dom z = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S₁[k,z . k] ) ) from FINSEQ_1:sch 5(A16);
A20: len s = len z by A11, A18, FINSEQ_1:def 3;
A22: dom z = dom D by FINSEQ_1:def 3, A18;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then lower_bound A = a by A7, INTEGRA1:5;
then consider i being Element of NAT such that
A50: i in dom D and
A51: t in divset (D,i) and
A52: ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) by A10, LM94;
t in [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A51, INTEGRA1:4;
then A53: ( lower_bound (divset (D,i)) <= t & t <= upper_bound (divset (D,i)) ) by XXREAL_1:1;
reconsider i = i as Nat ;
A54: i in Seg (len D) by A50, FINSEQ_1:def 3;
then consider si being Function of A,REAL such that
A55: ( si = s . i & z . i = si . t ) by A18;
i in Seg (len s) by A11, A50, FINSEQ_1:def 3;
then B56: i in dom s by FINSEQ_1:def 3;
set r = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)));
A57: ( 1 <= i & i <= len D ) by A50, FINSEQ_3:25;
then i + 0 <= (len D) + 1 by XREAL_1:7;
then A58: i in Seg ((len D) + 1) by A57;
b: ( 1 + 0 <= i + 1 & i <= len D ) by A54, FINSEQ_1:1, XREAL_1:7;
then i + 1 <= (len D) + 1 by XREAL_1:7;
then A59: i + 1 in Seg ((len D) + 1) by b;
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))

proof

set f0 = [.a,b.] --> 0;
set f1 = ([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0);
set g1 = [.a,(D . i).] --> 1;
set g2 = ].(D . i),b.] --> 0;
set f2 = ([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0);
set h1 = [.a,(D . (i - 1)).] --> 1;
set h2 = ].(D . (i - 1)),b.] --> 0;
B0: ( dom ([.a,b.] --> 0) = [.a,b.] & dom ([.a,(D . i).] --> 1) = [.a,(D . i).] & dom (].(D . i),b.] --> 0) = ].(D . i),b.] & dom ([.a,(D . (i - 1)).] --> 1) = [.a,(D . (i - 1)).] & dom (].(D . (i - 1)),b.] --> 0) = ].(D . (i - 1)),b.] ) by FUNCOP_1:13;

per cases ( i = 1 or i <> 1 ) ;

suppose A62: i = 1 ; :: thesis: z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A63: lower_bound A = a by A7, INTEGRA1:5;
A64: a in [.a,b.] by A7;
A65: D . i in [.a,b.] by A7, A50, INTEGRA1:6;
A66: ( lower_bound (divset (D,i)) = lower_bound A & upper_bound (divset (D,i)) = D . i ) by A50, A62, INTEGRA1:def 4;
A69: Dp1 (m,D,(i + 1)) = m . (D . ((i + 1) - 1)) by A59, defDp1, A62
.= ([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) by A8, A65, A10, A62 ;
A70: Dp1 (m,D,i) = m . (lower_bound A) by A58, A62, defDp1
.= [.a,b.] --> 0 by A8, A63, A64 ;
A72: dom ([.a,b.] --> 0) = A by A7, FUNCOP_1:13;
A73: ( a <= D . i & D . i <= b ) by A65, XXREAL_1:1;
A74: dom (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) = (dom ([.a,(D . i).] --> 1)) \/ (dom (].(D . i),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B0, A73, XXREAL_1:167 ;
rng ([.a,b.] --> 0) c= REAL ;
then reconsider f0 = [.a,b.] --> 0 as Function of A,REAL by A72, FUNCT_2:2;
rng (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) as Function of A,REAL by A74, FUNCT_2:2;
A76: si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))

proof

reconsider H = (Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) by A55, B56, A12;
then si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * H by Lm1;
then si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (h . t) by C0SP1:30
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t)) by A2, A69, A70, C0SP1:34 ;
hence si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t)) ; :: thesis: verum

end;

A77: t in [.a,(D . i).] by A63, A66, INTEGRA1:4, A51;
then A79: f1 . t = ([.a,(D . i).] --> 1) . t by FUNCT_4:16, B0, XXREAL_1:90
.= 1 by A77, FUNCOP_1:7 ;
f0 . t = 0 by A7, FUNCOP_1:7;
hence z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i))) by A55, A76, A79; :: thesis: verum

end;

suppose A80: i <> 1 ; :: thesis: z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))

then A82: D . (i - 1) in [.a,b.] by A7, A50, INTEGRA1:7;
A81: D . i in [.a,b.] by A7, A50, INTEGRA1:6;
A83: ( lower_bound (divset (D,i)) = D . (i - 1) & upper_bound (divset (D,i)) = D . i ) by A50, A80, INTEGRA1:def 4;
i - 1 in dom D by A50, A80, INTEGRA1:7;
then A86: D . (i - 1) < D . i by A50, XREAL_1:146, VALUED_0:def 13;
( D . (i - 1) = a or D . (i - 1) in ].a,b.] ) by A80, A7, A50, INTEGRA1:7, XXREAL_1:6;

per cases then ( a = D . (i - 1) or a < D . (i - 1) ) by XXREAL_1:2;

suppose A88: a = D . (i - 1) ; :: thesis: z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))

1 + 0 < i + 1 by XREAL_1:8, A57;
then A90: Dp1 (m,D,(i + 1)) = m . (D . ((i + 1) - 1)) by A59, defDp1
.= ([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) by A8, A81, A88, A86 ;
A91: Dp1 (m,D,i) = m . (D . (i - 1)) by A58, A80, defDp1
.= [.a,b.] --> 0 by A8, A82, A88 ;
A93: dom ([.a,b.] --> 0) = A by A7, FUNCOP_1:13;
A94: ( a <= D . i & D . i <= b ) by A81, XXREAL_1:1;
A96: dom (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) = (dom ([.a,(D . i).] --> 1)) \/ (dom (].(D . i),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B0, A94, XXREAL_1:167 ;
rng ([.a,b.] --> 0) c= REAL ;
then reconsider f0 = [.a,b.] --> 0 as Function of A,REAL by A93, FUNCT_2:2;
rng (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) as Function of A,REAL by A96, FUNCT_2:2;
A98: si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))

proof

reconsider H = (Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) by A55, B56, A12;
then si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * H by Lm1;
then si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (h . t) by C0SP1:30
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t)) by A2, A90, A91, C0SP1:34 ;
hence si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t)) ; :: thesis: verum

end;

A99: t in [.(D . (i - 1)),(D . i).] by A83, INTEGRA1:4, A51;
( a <= D . (i - 1) & D . (i - 1) <= b ) by A82, XXREAL_1:1;
then B100: [.(D . (i - 1)),(D . i).] c= [.a,(D . i).] by XXREAL_1:34;
then A102: f1 . t = ([.a,(D . i).] --> 1) . t by A99, FUNCT_4:16, B0, XXREAL_1:90
.= 1 by B100, A99, FUNCOP_1:7 ;
f0 . t = 0 by A7, FUNCOP_1:7;
hence z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i))) by A55, A98, A102; :: thesis: verum

end;

suppose A103: a < D . (i - 1) ; :: thesis: z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))

1 + 0 < i + 1 by XREAL_1:8, A57;
then A105: Dp1 (m,D,(i + 1)) = m . (D . ((i + 1) - 1)) by A59, defDp1
.= ([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) by A8, A81, A103, A86 ;
A106: Dp1 (m,D,i) = m . (D . (i - 1)) by A58, A80, defDp1
.= ([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0) by A8, A82, A103 ;
A108: ( a <= D . i & D . i <= b ) by A81, XXREAL_1:1;
A109: ( a <= D . (i - 1) & D . (i - 1) <= b ) by A82, XXREAL_1:1;
A110: dom (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) = (dom ([.a,(D . i).] --> 1)) \/ (dom (].(D . i),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B0, A108, XXREAL_1:167 ;
A111: dom (([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0)) = (dom ([.a,(D . (i - 1)).] --> 1)) \/ (dom (].(D . (i - 1)),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B0, A109, XXREAL_1:167 ;
rng (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) as Function of A,REAL by A110, FUNCT_2:2;
rng (([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0)) c= REAL ;
then reconsider f2 = ([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0) as Function of A,REAL by A111, FUNCT_2:2;
A112: ( a <= t & t <= b ) by XXREAL_1:1, A7;
A113: si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f2 . t))

proof

reconsider H = (Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) by A55, B56, A12;
then si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * H by Lm1;
then si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (h . t) by C0SP1:30
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f2 . t)) by A2, A105, A106, C0SP1:34 ;
hence si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f2 . t)) ; :: thesis: verum

end;

A114: t in [.(D . (i - 1)),(D . i).] by A83, INTEGRA1:4, A51;
B115: [.(D . (i - 1)),(D . i).] c= [.a,(D . i).] by A109, XXREAL_1:34;
then A117: f1 . t = ([.a,(D . i).] --> 1) . t by A114, FUNCT_4:16, B0, XXREAL_1:90
.= 1 by B115, A114, FUNCOP_1:7 ;
( D . (i - 1) < t & t <= D . i ) by A50, A80, INTEGRA1:def 4, A52;
then A118: t in ].(D . (i - 1)),b.] by A112;
then f2 . t = (].(D . (i - 1)),b.] --> 0) . t by B0, FUNCT_4:13
.= 0 by A118, FUNCOP_1:7 ;
hence z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i))) by A55, A113, A117; :: thesis: verum

end;

end;

end;

end;

end;

then A119: |.(z . i).| <= 1 by LM91;
for k being Nat st k in dom z & k <> i holds
z . k = 0

proof

let k be Nat; :: thesis: ( k in dom z & k <> i implies z . k = 0 )
assume that
A120: k in dom z and
A121: k <> i ; :: thesis: z . k = 0
consider sk being Function of A,REAL such that
A124: ( sk = s . k & z . k = sk . t ) by A18, A120;
B125: k in dom s by FINSEQ_1:def 3, A11, A18, A120;
then A125: s . k = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k))) by A12;
set r = sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)));
A126: k in dom D by A18, A120, FINSEQ_1:def 3;
then A127: ( 1 <= k & k <= len D ) by FINSEQ_3:25;
then k + 0 <= (len D) + 1 by XREAL_1:7;
then A128: k in Seg ((len D) + 1) by A127;
a: 1 + 0 <= k + 1 by XREAL_1:7;
k + 1 <= (len D) + 1 by A127, XREAL_1:7;
then A129: k + 1 in Seg ((len D) + 1) by a;
set f0 = [.a,b.] --> 0;
set f1 = ([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0);
set g1 = [.a,(D . k).] --> 1;
set g2 = ].(D . k),b.] --> 0;
set f2 = ([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0);
set h1 = [.a,(D . (k - 1)).] --> 1;
set h2 = ].(D . (k - 1)),b.] --> 0;
B10: ( dom ([.a,b.] --> 0) = [.a,b.] & dom ([.a,(D . k).] --> 1) = [.a,(D . k).] & dom (].(D . k),b.] --> 0) = ].(D . k),b.] & dom ([.a,(D . (k - 1)).] --> 1) = [.a,(D . (k - 1)).] & dom (].(D . (k - 1)),b.] --> 0) = ].(D . (k - 1)),b.] ) by FUNCOP_1:13;

per cases ( k = 1 or k <> 1 ) ;

suppose A130: k = 1 ; :: thesis: z . k = 0

then A134: ( lower_bound (divset (D,i)) = D . (i - 1) & upper_bound (divset (D,i)) = D . i ) by A50, INTEGRA1:def 4, A121;
A136: i - 1 in dom D by A50, INTEGRA1:7, A130, A121;
A141: D . k in [.a,b.] by A7, A126, INTEGRA1:6;
then A147: ( a <= D . k & D . k <= b ) by XXREAL_1:1;
A146: dom ([.a,b.] --> 0) = A by A7, FUNCOP_1:13;
A148: dom (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) = (dom ([.a,(D . k).] --> 1)) \/ (dom (].(D . k),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B10, A147, XXREAL_1:167 ;
rng ([.a,b.] --> 0) c= REAL ;
then reconsider f0 = [.a,b.] --> 0 as Function of A,REAL by A146, FUNCT_2:2;
rng (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0) as Function of A,REAL by A148, FUNCT_2:2;
A153: Dp1 (m,D,(k + 1)) = m . (D . ((k + 1) - 1)) by A129, defDp1, A130
.= ([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0) by A8, A141, A10, A130 ;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A139: lower_bound A = a by A7, INTEGRA1:5;
A140: a in [.a,b.] by A7;
A144: Dp1 (m,D,k) = m . (lower_bound A) by A128, A130, defDp1
.= [.a,b.] --> 0 by A8, A139, A140 ;
A154: sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f0 . t))

proof

reconsider H = (Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
sk = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k))) by A124, B125, A12;
then sk = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * H by Lm1;
then sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * (h . t) by C0SP1:30
.= (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f0 . t)) by A2, A144, A153, C0SP1:34 ;
hence sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f0 . t)) ; :: thesis: verum

end;

k < i by A130, A121, A57, XXREAL_0:1;
then k + 1 <= i by NAT_1:13;
then A157: (k + 1) - 1 <= i - 1 by XREAL_1:13;
D . k <= D . (i - 1)

proof

( k = i - 1 or k < i - 1 ) by A157, XXREAL_0:1;
hence D . k <= D . (i - 1) by A126, A136, VALUED_0:def 13; :: thesis: verum

end;

then A158: D . k < t by A52, A130, A121, XXREAL_0:2, A134;
( a <= t & t <= b ) by XXREAL_1:1, A7;
then A160: t in ].(D . k),b.] by A158;
then A162: f1 . t = (].(D . k),b.] --> 0) . t by B10, FUNCT_4:13
.= 0 by A160, FUNCOP_1:7 ;
f0 . t = 0 by A7, FUNCOP_1:7;
hence z . k = 0 by A124, A154, A162; :: thesis: verum

end;

suppose A163: k <> 1 ; :: thesis: z . k = 0

then A165: D . (k - 1) in [.a,b.] by A7, A126, INTEGRA1:7;
A164: D . k in [.a,b.] by A7, A126, INTEGRA1:6;
A168: k - 1 in dom D by A126, A163, INTEGRA1:7;
then A169: D . (k - 1) < D . k by A126, XREAL_1:146, VALUED_0:def 13;
1 < k by A127, A163, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A171: 2 - 1 <= k - 1 by XREAL_1:13;
1 <= len D by A127, XXREAL_0:2;
then A172: 1 in dom D by FINSEQ_3:25;
B173: D . 1 <= D . (k - 1)

proof

( 1 = k - 1 or 1 < k - 1 ) by A171, XXREAL_0:1;
hence D . 1 <= D . (k - 1) by A168, A172, VALUED_0:def 13; :: thesis: verum

end;

then A173: a < D . (k - 1) by A10, XXREAL_0:2;
1 + 0 < k + 1 by XREAL_1:8, A127;
then A175: Dp1 (m,D,(k + 1)) = m . (D . ((k + 1) - 1)) by A129, defDp1
.= ([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0) by A8, A164, A173, A169 ;
A176: Dp1 (m,D,k) = m . (D . (k - 1)) by A128, A163, defDp1
.= ([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0) by A8, A165, B173, A10 ;
A178: ( a <= D . k & D . k <= b ) by A164, XXREAL_1:1;
A179: ( a <= D . (k - 1) & D . (k - 1) <= b ) by A165, XXREAL_1:1;
A180: dom (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) = (dom ([.a,(D . k).] --> 1)) \/ (dom (].(D . k),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B10, A178, XXREAL_1:167 ;
A181: dom (([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0)) = (dom ([.a,(D . (k - 1)).] --> 1)) \/ (dom (].(D . (k - 1)),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B10, A179, XXREAL_1:167 ;
rng (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0) as Function of A,REAL by A180, FUNCT_2:2;
rng (([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0)) c= REAL ;
then reconsider f2 = ([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0) as Function of A,REAL by A181, FUNCT_2:2;
A183: sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f2 . t))

proof

reconsider H = (Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
sk = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * H by Lm1, A124, A125;
then sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * (h . t) by C0SP1:30
.= (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f2 . t)) by A2, A175, A176, C0SP1:34 ;
hence sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f2 . t)) ; :: thesis: verum

end;

per cases ( i < k or k < i ) by A121, XXREAL_0:1;

suppose i < k ; :: thesis: z . k = 0

then i + 1 <= k by NAT_1:13;
then A186: (i + 1) - 1 <= k - 1 by XREAL_1:13;
A187: D . i <= D . (k - 1)

proof

( i = k - 1 or i < k - 1 ) by A186, XXREAL_0:1;
hence D . i <= D . (k - 1) by A50, A168, VALUED_0:def 13; :: thesis: verum

end;

A189: upper_bound (divset (D,i)) <= D . (k - 1)

proof

per cases ( i = 1 or i <> 1 ) ;

suppose i = 1 ; :: thesis: upper_bound (divset (D,i)) <= D . (k - 1)

hence upper_bound (divset (D,i)) <= D . (k - 1) by A187, A50, INTEGRA1:def 4; :: thesis: verum

end;

suppose i <> 1 ; :: thesis: upper_bound (divset (D,i)) <= D . (k - 1)

hence upper_bound (divset (D,i)) <= D . (k - 1) by A187, A50, INTEGRA1:def 4; :: thesis: verum

end;

end;

end;

A191: ( a <= t & t <= D . (k - 1) ) by A189, XXREAL_0:2, A53, XXREAL_1:1, A7;
then A192: t in [.a,(D . (k - 1)).] ;
( a <= t & t <= D . k ) by A169, A191, XXREAL_0:2;
then A193: t in [.a,(D . k).] ;
then A196: f1 . t = ([.a,(D . k).] --> 1) . t by FUNCT_4:16, B10, XXREAL_1:90
.= 1 by A193, FUNCOP_1:7 ;
f2 . t = ([.a,(D . (k - 1)).] --> 1) . t by B10, A192, FUNCT_4:16, XXREAL_1:90
.= 1 by A192, FUNCOP_1:7 ;
hence z . k = 0 by A124, A183, A196; :: thesis: verum

end;

suppose A198: k < i ; :: thesis: z . k = 0

then k + 1 <= i by NAT_1:13;
then A201: (k + 1) - 1 <= i - 1 by XREAL_1:13;
A202: i - 1 in dom D by A50, A198, A127, INTEGRA1:7;
A203: ( lower_bound (divset (D,i)) = D . (i - 1) & upper_bound (divset (D,i)) = D . i ) by A50, A198, A127, INTEGRA1:def 4;
D . k <= D . (i - 1)

proof

( k = i - 1 or k < i - 1 ) by A201, XXREAL_0:1;
hence D . k <= D . (i - 1) by A126, A202, VALUED_0:def 13; :: thesis: verum

end;

then A206: D . k < t by A198, A52, A18, A120, FINSEQ_1:1, XXREAL_0:2, A203;
then A207: D . (k - 1) < t by A169, XXREAL_0:2;
A208: ( a <= t & t <= b ) by XXREAL_1:1, A7;
then A209: t in ].(D . k),b.] by A206;
then A211: f1 . t = (].(D . k),b.] --> 0) . t by B10, FUNCT_4:13
.= 0 by A209, FUNCOP_1:7 ;
A210: t in ].(D . (k - 1)),b.] by A207, A208;
then f2 . t = (].(D . (k - 1)),b.] --> 0) . t by B10, FUNCT_4:13
.= 0 by A210, FUNCOP_1:7 ;
hence z . k = 0 by A124, A183, A211; :: thesis: verum

end;

end;

end;

end;

end;

then |.(Sum z).| <= 1 by A22, A50, A119, INTEGR23:6;
hence |.(g . t).| <= 1 by A13, A20, LM89, A18; :: thesis: verum

end;

now :: thesis: for k being Real st k in PreNorms g holds
k <= 1

let k be Real; :: thesis: ( k in PreNorms g implies k <= 1 )
assume k in PreNorms g ; :: thesis: k <= 1
then consider t being Element of A such that
A213: k = |.(g . t).| ;
thus k <= 1 by A15, A213; :: thesis: verum

end;

then upper_bound (PreNorms g) <= 1 by SEQ_4:45;
then (BoundedFunctionsNorm A) . g <= 1 by A13, C0SP1:20;
then A214: ||.(Sum s).|| <= 1 by A13, Lm1;
A215: ( len K = len D & ( for i being Nat st i in dom D holds
K . i = |.(vol ((divset (D,i)),rho)).| ) ) by INTEGR22:def 2;
dom f = the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by FUNCT_2:def 1;
then rng s c= dom f ;
then A216: dom (f * s) = dom s by RELAT_1:27
.= Seg (len s) by FINSEQ_1:def 3
.= dom K by A11, A215, FINSEQ_1:def 3 ;
A217: for i being Nat st i in dom D holds
(f * s) . i = |.(vol ((divset (D,i)),rho)).|

proof

let i be Nat; :: thesis: ( i in dom D implies (f * s) . i = |.(vol ((divset (D,i)),rho)).| )
assume A218: i in dom D ; :: thesis: (f * s) . i = |.(vol ((divset (D,i)),rho)).|
then A220: ( 1 <= i & i <= len D ) by FINSEQ_3:25;
then i + 0 <= (len D) + 1 by XREAL_1:7;
then A221: i in Seg ((len D) + 1) by A220;
b: 1 + 0 <= i + 1 by XREAL_1:7;
i + 1 <= (len D) + 1 by A220, XREAL_1:7;
then A222: i + 1 in Seg ((len D) + 1) by b;
i in Seg (len s) by A11, A218, FINSEQ_1:def 3;
then A223: i in dom s by FINSEQ_1:def 3;
set r = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)));
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A224: lower_bound A = a by A7, INTEGRA1:5;
D . i in A by A218, INTEGRA1:6;
then A225: D . i in dom m by FUNCT_2:def 1;
lower_bound A in A by A7, A224;
then A226: lower_bound A in dom m by FUNCT_2:def 1;

per cases ( i = 1 or i <> 1 ) ;

suppose A227: i = 1 ; :: thesis: (f * s) . i = |.(vol ((divset (D,i)),rho)).|

then A228: ( lower_bound (divset (D,i)) = lower_bound A & upper_bound (divset (D,i)) = D . i ) by A218, INTEGRA1:def 4;
A229: Dp1 (m,D,(i + 1)) = m . (D . ((i + 1) - 1)) by A222, defDp1, A227
.= m . (D . i) ;
A231: (f * s) . i = f . (s . i) by A223, FUNCT_1:13
.= f . ((sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))) by A12, A223
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (f . ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))) by HAHNBAN:def 3
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (Dp1 (m,D,(i + 1)))) - (f . (Dp1 (m,D,i)))) by HAHNBAN:19
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (m . (D . i))) - (f . (m . (lower_bound A)))) by A229, A221, A227, defDp1
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (((f * m) . (D . i)) - (f . (m . (lower_bound A)))) by A225, FUNCT_1:13
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i))))) by A228, A226, FUNCT_1:13
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (vol ((divset (D,i)),rho)) by INTEGR22:def 1 ;
A232: Dp2 (rho,D,(i + 1)) = rho . (D . ((i + 1) - 1)) by defDp2, A227
.= rho . (D . i) ;
sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i))) = sgn ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i))))) by A228, A232, A227, defDp2
.= sgn (vol ((divset (D,i)),rho)) by INTEGR22:def 1 ;
hence (f * s) . i = |.(vol ((divset (D,i)),rho)).| by A231, LM86; :: thesis: verum

end;

suppose A234: i <> 1 ; :: thesis: (f * s) . i = |.(vol ((divset (D,i)),rho)).|

D . i in A by A218, INTEGRA1:6;
then A235: D . i in dom m by FUNCT_2:def 1;
D . (i - 1) in A by A218, A234, INTEGRA1:7;
then A236: D . (i - 1) in dom m by FUNCT_2:def 1;
A237: ( lower_bound (divset (D,i)) = D . (i - 1) & upper_bound (divset (D,i)) = D . i ) by A218, A234, INTEGRA1:def 4;
A238: 1 + 0 < i + 1 by XREAL_1:8, A220;
then A239: Dp1 (m,D,(i + 1)) = m . (D . ((i + 1) - 1)) by A222, defDp1
.= m . (D . i) ;
A241: (f * s) . i = f . (s . i) by A223, FUNCT_1:13
.= f . ((sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))) by A12, A223
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (f . ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))) by HAHNBAN:def 3
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (Dp1 (m,D,(i + 1)))) - (f . (Dp1 (m,D,i)))) by HAHNBAN:19
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (m . (D . i))) - (f . (m . (D . (i - 1))))) by A239, A221, A234, defDp1
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (((f * m) . (D . i)) - (f . (m . (D . (i - 1))))) by A235, FUNCT_1:13
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i))))) by A237, A236, FUNCT_1:13
.= (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (vol ((divset (D,i)),rho)) by INTEGR22:def 1 ;
A242: Dp2 (rho,D,(i + 1)) = rho . (D . ((i + 1) - 1)) by A238, defDp2
.= rho . (D . i) ;
sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i))) = sgn ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i))))) by A237, A242, A234, defDp2
.= sgn (vol ((divset (D,i)),rho)) by INTEGR22:def 1 ;
hence (f * s) . i = |.(vol ((divset (D,i)),rho)).| by A241, LM86; :: thesis: verum

end;

end;

end;

for i being Nat st i in dom K holds
(f * s) . i = K . i

proof

let i be Nat; :: thesis: ( i in dom K implies (f * s) . i = K . i )
assume i in dom K ; :: thesis: (f * s) . i = K . i
then i in Seg (len D) by A215, FINSEQ_1:def 3;
then A244: i in dom D by FINSEQ_1:def 3;
then K . i = |.(vol ((divset (D,i)),rho)).| by INTEGR22:def 2;
hence (f * s) . i = K . i by A217, A244; :: thesis: verum

end;

then A245: f . (Sum s) = Sum K by A14, A216, FINSEQ_1:13;
A246: f . (Sum s) <= |.(f . (Sum s)).| by ABSVALUE:4;
A247: |.(f . (Sum s)).| <= ||.F.|| * ||.(Sum s).|| by A6, DUALSP01:26;
||.F.|| * ||.(Sum s).|| <= ||.F.|| * 1 by A214, XREAL_1:64;
then |.(f . (Sum s)).| <= ||.F.|| by A247, XXREAL_0:2;
hence Sum K <= ||.x.|| by A6, A245, A246, XXREAL_0:2; :: thesis: verum

end;

reconsider d = ||.x.|| + 1 as Real ;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A249: lower_bound A = a by A7, INTEGRA1:5;
then for D being Division of A
for K being var_volume of rho,D holds Sum K <= ||.x.|| by A1, A9, LM95;
then B250: for t being Division of A
for F0 being var_volume of rho,t holds Sum F0 <= d by XREAL_1:39;
then A251: rho is bounded_variation ;
then consider VD being non empty Subset of REAL such that
VD is bounded_above and
A253: VD = { r where r is Real : ex t being Division of A ex F0 being var_volume of rho,t st r = Sum F0 } and
A254: total_vd rho = upper_bound VD by INTEGR22:def 4;

now :: thesis: for k being Real st k in VD holds
k <= ||.x.||

let k be Real; :: thesis: ( k in VD implies k <= ||.x.|| )
assume k in VD ; :: thesis: k <= ||.x.||
then consider r being Real such that
A255: k = r and
A256: ex t being Division of A ex F0 being var_volume of rho,t st r = Sum F0 by A253;
consider t being Division of A, F0 being var_volume of rho,t such that
A257: r = Sum F0 by A256;
thus k <= ||.x.|| by A249, A1, A9, LM95, A255, A257; :: thesis: verum

end;

then A258: total_vd rho <= ||.x.|| by A254, SEQ_4:45;
A259: for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho)

proof

let u be continuous PartFunc of REAL,REAL; :: thesis: ( dom u = A implies x . u = integral (u,rho) )
assume A260: dom u = A ; :: thesis: x . u = integral (u,rho)
then A261: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (u | A) & x2 in dom (u | A) & |.(x1 - x2).| < s holds
|.(((u | A) . x1) - ((u | A) . x2)).| < r ) ) by FCONT_2:def 1, FCONT_2:11;
B262: u is_RiemannStieltjes_integrable_with rho by A251, A260, INTEGR23:21;
consider T being DivSequence of A such that
A263: ( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) by A1, INTEGRA6:16;
A264: for n being Nat holds a < (T . n) . 1

proof

let n be Nat; :: thesis: a < (T . n) . 1
n is Element of NAT by ORDINAL1:def 12;
then consider Tn being Division of A such that
A265: ( Tn divide_into_equal n + 1 & T . n = Tn ) by A263;
A266: len Tn = n + 1 by A265, INTEGRA4:def 1;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then ( 1 <= n + 1 & n + 1 <= len Tn ) by FINSEQ_1:1, A265, INTEGRA4:def 1;
then 1 <= len Tn by XXREAL_0:2;
then B268: 1 in dom Tn by FINSEQ_3:25;
0 < (vol A) / (len Tn) by A1, A266, XREAL_1:139;
then (lower_bound A) + 0 < (lower_bound A) + (((vol A) / (len Tn)) * 1) by XREAL_1:8;
hence a < (T . n) . 1 by A265, A249, B268, INTEGRA4:def 1; :: thesis: verum

end;

set S = the middle_volume_Sequence of rho,u,T;
A269: u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) by A260, Th80;
defpred S₁[ 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) & ( the middle_volume_Sequence of rho,u,T . $1) . i = z * (vol ((divset ((T . $1),i)),rho)) ) ) ) );
A270: for k being Element of NAT ex p being Element of REAL * st S₁[k,p]

proof

let k be Element of NAT ; :: thesis: ex p being Element of REAL * st S₁[k,p]
defpred S₂[ Nat, set ] means ( $2 in dom (u | (divset ((T . k),$1))) & ex c being Real st
( c = (u | (divset ((T . k),$1))) . $2 & ( the middle_volume_Sequence of rho,u,T . k) . $1 = c * (vol ((divset ((T . k),$1)),rho)) ) );
A271: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;
A272: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of REAL st S₂[i,x]

proof

let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S₂[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S₂[i,x]
then i in dom (T . k) by FINSEQ_1:def 3;
then consider c being Real such that
A273: ( c in rng (u | (divset ((T . k),i))) & ( the middle_volume_Sequence of rho,u,T . k) . i = c * (vol ((divset ((T . k),i)),rho)) ) by A251, A260, INTEGR22:def 5;
consider x being object such that
A274: ( x in dom (u | (divset ((T . k),i))) & c = (u | (divset ((T . k),i))) . x ) by A273, FUNCT_1:def 3;
reconsider x = x as Element of REAL by A274;
take x ; :: thesis: S₂[i,x]
thus S₂[i,x] by A273, A274; :: thesis: verum

end;

consider p being FinSequence of REAL such that
A275: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S₂[i,p . i] ) ) from FINSEQ_1:sch 5(A272);
take p ; :: thesis: ( p is Element of REAL * & S₁[k,p] )
len p = len (T . k) by A275, FINSEQ_1:def 3;
hence ( p is Element of REAL * & S₁[k,p] ) by A271, A275, FINSEQ_1:def 11; :: thesis: verum

end;

consider F being sequence of (REAL *) such that
A276: for x being Element of NAT holds S₁[x,F . x] from FUNCT_2:sch 3(A270);
defpred S₂[ Element of NAT , object ] means ex q being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
( len q = len (T . $1) & $2 = Sum q & ( for i being Nat st i in dom (T . $1) holds
ex r being Real st
( (F . $1) . i in dom (u | (divset ((T . $1),i))) & r = (u | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = r * ((Dp1 (m,(T . $1),(i + 1))) - (Dp1 (m,(T . $1),i))) ) ) );
A277: for k being Element of NAT ex x being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S₂[k,x]

proof

let k be Element of NAT ; :: thesis: ex x being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S₂[k,x]
defpred S₃[ Nat, object ] means ex r being Real st
( (F . k) . $1 in dom (u | (divset ((T . k),$1))) & r = (u | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = r * ((Dp1 (m,(T . k),($1 + 1))) - (Dp1 (m,(T . k),$1))) );
A278: for i being Nat st i in Seg (len (T . k)) holds
ex y being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S₃[i,y]

proof

let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex y being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S₃[i,y] )
assume i in Seg (len (T . k)) ; :: thesis: ex y being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S₃[i,y]
then A279: i in dom (T . k) by FINSEQ_1:def 3;
consider p being FinSequence of REAL such that
A280: ( 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) & ( the middle_volume_Sequence of rho,u,T . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) ) by A276;
p . i in dom (u | (divset ((T . k),i))) by A279, A280;
then (u | (divset ((T . k),i))) . (p . i) in rng (u | (divset ((T . k),i))) by FUNCT_1:3;
then reconsider r = (u | (divset ((T . k),i))) . (p . i) as Element of REAL ;
r * ((Dp1 (m,(T . k),(i + 1))) - (Dp1 (m,(T . k),i))) is Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
hence ex y being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S₃[i,y] by A280, A279; :: thesis: verum

end;

consider q being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that
A282: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S₃[i,q . i] ) ) from FINSEQ_1:sch 5(A278);
take x = Sum q; :: thesis: S₂[k,x]
A283: dom (T . k) = Seg (len (T . k)) by FINSEQ_1:def 3;
len q = len (T . k) by A282, FINSEQ_1:def 3;
hence S₂[k,x] by A282, A283; :: thesis: verum

end;

consider xD being sequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that
A284: for z being Element of NAT holds S₂[z,xD . z] from FUNCT_2:sch 3(A277);
B314: for n being Element of NAT holds (f * xD) . n = (middle_sum the middle_volume_Sequence of rho,u,T) . n

proof

let n be Element of NAT ; :: thesis: (f * xD) . n = (middle_sum the middle_volume_Sequence of rho,u,T) . n
consider p1 being FinSequence of REAL such that
A285: ( p1 = F . n & len p1 = len (T . n) & ( for i being Nat st i in dom (T . n) holds
( p1 . i in dom (u | (divset ((T . n),i))) & ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & ( the middle_volume_Sequence of rho,u,T . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) ) by A276;
consider q1 being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that
A286: ( len q1 = len (T . n) & xD . n = Sum q1 & ( for i being Nat st i in dom (T . n) holds
ex r being Real st
( (F . n) . i in dom (u | (divset ((T . n),i))) & r = (u | (divset ((T . n),i))) . ((F . n) . i) & q1 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i))) ) ) ) by A284;
A287: (middle_sum the middle_volume_Sequence of rho,u,T) . n = Sum ( the middle_volume_Sequence of rho,u,T . n) by INTEGR22:def 7;
dom xD = NAT by FUNCT_2:def 1;
then A288: (f * xD) . n = f . (Sum q1) by A286, FUNCT_1:13
.= Sum (f * q1) by LM87 ;
dom f = the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by FUNCT_2:def 1;
then rng q1 c= dom f ;
then dom (f * q1) = dom q1 by RELAT_1:27
.= Seg (len q1) by FINSEQ_1:def 3
.= Seg (len ( the middle_volume_Sequence of rho,u,T . n)) by A251, A260, A286, INTEGR22:def 5 ;
then A289: len (f * q1) = len ( the middle_volume_Sequence of rho,u,T . n) by FINSEQ_1:def 3;
for k being Nat st 1 <= k & k <= len ( the middle_volume_Sequence of rho,u,T . n) holds
(f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ( the middle_volume_Sequence of rho,u,T . n) implies (f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k )
assume A290: ( 1 <= k & k <= len ( the middle_volume_Sequence of rho,u,T . n) ) ; :: thesis: (f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k
then B291: k in Seg (len ( the middle_volume_Sequence of rho,u,T . n)) ;
then k in Seg (len (T . n)) by A251, A260, INTEGR22:def 5;
then A292: k in dom (T . n) by FINSEQ_1:def 3;
then consider z being Real such that
A293: ( z = (u | (divset ((T . n),k))) . ((F . n) . k) & ( the middle_volume_Sequence of rho,u,T . n) . k = z * (vol ((divset ((T . n),k)),rho)) ) by A285;
consider r being Real such that
A294: ( (F . n) . k in dom (u | (divset ((T . n),k))) & r = (u | (divset ((T . n),k))) . ((F . n) . k) & q1 . k = r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))) ) by A286, A292;
( 1 <= k & k <= len (T . n) ) by A251, A260, A290, INTEGR22:def 5;
then k + 0 <= (len (T . n)) + 1 by XREAL_1:7;
then A296: k in Seg ((len (T . n)) + 1) by A290;
d: ( 1 + 0 <= k + 1 & k <= len (T . n) ) by A251, A260, A290, INTEGR22:def 5, XREAL_1:7;
then k + 1 <= (len (T . n)) + 1 by XREAL_1:7;
then A297: k + 1 in Seg ((len (T . n)) + 1) by d;
k in Seg (len q1) by A286, B291, A251, A260, INTEGR22:def 5;
then A298: k in dom q1 by FINSEQ_1:def 3;

per cases ( k = 1 or k <> 1 ) ;

suppose A299: k = 1 ; :: thesis: (f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then lower_bound A = a by A7, INTEGRA1:5;
then lower_bound A in A by A7;
then A301: lower_bound A in dom m by FUNCT_2:def 1;
(T . n) . k in A by A292, INTEGRA1:6;
then A302: (T . n) . k in dom m by FUNCT_2:def 1;
A303: ( lower_bound (divset ((T . n),k)) = lower_bound A & upper_bound (divset ((T . n),k)) = (T . n) . k ) by A292, A299, INTEGRA1:def 4;
A304: Dp1 (m,(T . n),(k + 1)) = m . ((T . n) . ((k + 1) - 1)) by A297, defDp1, A299
.= m . ((T . n) . k) ;
A306: f . ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))) = (f . (Dp1 (m,(T . n),(k + 1)))) - (f . (Dp1 (m,(T . n),k))) by HAHNBAN:19
.= (f . (m . ((T . n) . k))) - (f . (m . (lower_bound A))) by A304, A296, A299, defDp1
.= ((f * m) . ((T . n) . k)) - (f . (m . (lower_bound A))) by A302, FUNCT_1:13
.= (rho . (upper_bound (divset ((T . n),k)))) - (rho . (lower_bound (divset ((T . n),k)))) by A303, A301, FUNCT_1:13
.= vol ((divset ((T . n),k)),rho) by INTEGR22:def 1 ;
thus (f * q1) . k = f . (r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k)))) by A294, A298, FUNCT_1:13
.= ( the middle_volume_Sequence of rho,u,T . n) . k by A293, A294, A306, HAHNBAN:def 3 ; :: thesis: verum

end;

suppose A307: k <> 1 ; :: thesis: (f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k

(T . n) . k in A by A292, INTEGRA1:6;
then A308: (T . n) . k in dom m by FUNCT_2:def 1;
(T . n) . (k - 1) in A by A292, A307, INTEGRA1:7;
then A309: (T . n) . (k - 1) in dom m by FUNCT_2:def 1;
A310: ( lower_bound (divset ((T . n),k)) = (T . n) . (k - 1) & upper_bound (divset ((T . n),k)) = (T . n) . k ) by A292, A307, INTEGRA1:def 4;
1 + 0 < k + 1 by XREAL_1:8, A290;
then A311: Dp1 (m,(T . n),(k + 1)) = m . ((T . n) . ((k + 1) - 1)) by A297, defDp1
.= m . ((T . n) . k) ;
A313: f . ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))) = (f . (Dp1 (m,(T . n),(k + 1)))) - (f . (Dp1 (m,(T . n),k))) by HAHNBAN:19
.= (f . (m . ((T . n) . k))) - (f . (m . ((T . n) . (k - 1)))) by A311, A296, A307, defDp1
.= ((f * m) . ((T . n) . k)) - (f . (m . ((T . n) . (k - 1)))) by A308, FUNCT_1:13
.= (rho . (upper_bound (divset ((T . n),k)))) - (rho . (lower_bound (divset ((T . n),k)))) by A310, A309, FUNCT_1:13
.= vol ((divset ((T . n),k)),rho) by INTEGR22:def 1 ;
thus (f * q1) . k = f . (r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k)))) by A294, A298, FUNCT_1:13
.= ( the middle_volume_Sequence of rho,u,T . n) . k by A293, A294, A313, HAHNBAN:def 3 ; :: thesis: verum

end;

end;

end;

hence (f * xD) . n = (middle_sum the middle_volume_Sequence of rho,u,T) . n by A287, A288, A289, FINSEQ_1:14; :: thesis: verum

end;

A315: ( middle_sum the middle_volume_Sequence of rho,u,T is convergent & lim (middle_sum the middle_volume_Sequence of rho,u,T) = integral (u,rho) ) by B262, A251, A260, INTEGR22:def 9, A263;
A316: u in BoundedFunctions the carrier of (ClstoCmp A) by A269, Lm2;
reconsider v = u as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by A269, Lm2;
v in BoundedFunctions A by A316, Lm1;
then consider g being Function of A,REAL such that
A317: ( g = v & g | A is bounded ) ;
reconsider v0 = v as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
A318: for r being Real st 0 < r holds
ex m0 being Nat st
for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m0 being Nat st
for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r )
assume A319: 0 < r ; :: thesis: ex m0 being Nat st
for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r
then A321: r / 2 < r by XREAL_1:216;
consider s being Real such that
A322: 0 < s and
A323: for x1, x2 being Real st x1 in dom (u | A) & x2 in dom (u | A) & |.(x1 - x2).| < s holds
|.(((u | A) . x1) - ((u | A) . x2)).| < r / 2 by A261, A319, XREAL_1:215;
consider m0 being Nat such that
A324: for i being Nat st m0 <= i holds
|.(((delta T) . i) - 0).| < s by A263, A322, SEQ_2:def 7;
A325: for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r

proof

let n be Nat; :: thesis: ( m0 <= n implies ||.((xD . n) - v0).|| < r )
A326: n in NAT by ORDINAL1:def 12;
consider p2 being FinSequence of REAL such that
A327: ( p2 = F . n & len p2 = len (T . n) & ( for i being Nat st i in dom (T . n) holds
( p2 . i in dom (u | (divset ((T . n),i))) & ex z being Real st
( z = (u | (divset ((T . n),i))) . (p2 . i) & ( the middle_volume_Sequence of rho,u,T . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) ) by A276, A326;
consider q2 being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that
A328: ( len q2 = len (T . n) & xD . n = Sum q2 & ( for i being Nat st i in dom (T . n) holds
ex r being Real st
( (F . n) . i in dom (u | (divset ((T . n),i))) & r = (u | (divset ((T . n),i))) . ((F . n) . i) & q2 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i))) ) ) ) by A284, A326;
assume m0 <= n ; :: thesis: ||.((xD . n) - v0).|| < r
then |.(((delta T) . n) - 0).| < s by A324;
then |.(delta (T . n)).| < s by A326, INTEGRA3:def 2;
then A329: delta (T . n) < s by ABSVALUE:def 1, INTEGRA3:9;
xD . n in the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
then xD . n in BoundedFunctions A by Lm1;
then consider g1 being Function of A,REAL such that
A330: ( g1 = xD . n & g1 | A is bounded ) ;
A331: for t being Element of A
for i being Nat st i in dom (T . n) & t in divset ((T . n),i) & ( i = 1 or ( lower_bound (divset ((T . n),i)) < t & t <= upper_bound (divset ((T . n),i)) ) ) holds
g1 . t = g . (p2 . i)

proof

let t be Element of A; :: thesis: for i being Nat st i in dom (T . n) & t in divset ((T . n),i) & ( i = 1 or ( lower_bound (divset ((T . n),i)) < t & t <= upper_bound (divset ((T . n),i)) ) ) holds
g1 . t = g . (p2 . i)
let i be Nat; :: thesis: ( i in dom (T . n) & t in divset ((T . n),i) & ( i = 1 or ( lower_bound (divset ((T . n),i)) < t & t <= upper_bound (divset ((T . n),i)) ) ) implies g1 . t = g . (p2 . i) )
assume that
A332: i in dom (T . n) and
A333: t in divset ((T . n),i) and
A334: ( i = 1 or ( lower_bound (divset ((T . n),i)) < t & t <= upper_bound (divset ((T . n),i)) ) ) ; :: thesis: g1 . t = g . (p2 . i)
consider r being Real such that
A336: p2 . i in dom (u | (divset ((T . n),i))) and
A337: r = (u | (divset ((T . n),i))) . (p2 . i) and
A338: q2 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i))) by A327, A328, A332;
defpred S₃[ Nat, set ] means ex qi being Function of A,REAL st
( qi = q2 . $1 & $2 = qi . t );
A340: for i being Nat st i in Seg (len (T . n)) holds
ex x being Element of REAL st S₃[i,x]

proof

let i be Nat; :: thesis: ( i in Seg (len (T . n)) implies ex x being Element of REAL st S₃[i,x] )
assume i in Seg (len (T . n)) ; :: thesis: ex x being Element of REAL st S₃[i,x]
then i in dom (T . n) by FINSEQ_1:def 3;
then consider r being Real such that
A342: ( p2 . i in dom (u | (divset ((T . n),i))) & r = (u | (divset ((T . n),i))) . (p2 . i) & q2 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i))) ) by A327, A328;
q2 . i in the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by A342;
then q2 . i in BoundedFunctions A by Lm1;
then consider qi being Function of A,REAL such that
A343: ( qi = q2 . i & qi | A is bounded ) ;
take x = qi . t; :: thesis: S₃[i,x]
thus S₃[i,x] by A343; :: thesis: verum

end;

consider z being FinSequence of REAL such that
A344: ( dom z = Seg (len (T . n)) & ( for i being Nat st i in Seg (len (T . n)) holds
S₃[i,z . i] ) ) from FINSEQ_1:sch 5(A340);
A346: len q2 = len z by A328, A344, FINSEQ_1:def 3;
A347: i in dom z by A344, A332, FINSEQ_1:def 3;
A348: g1 . t = Sum z by A328, A330, A346, LM89, A344;
A349: dom z = dom (T . n) by FINSEQ_1:def 3, A344;
A350: i in Seg (len (T . n)) by A332, FINSEQ_1:def 3;
then consider qi being Function of A,REAL such that
A351: ( qi = q2 . i & z . i = qi . t ) by A344;
set D = T . n;
B352: t in [.(lower_bound (divset ((T . n),i))),(upper_bound (divset ((T . n),i))).] by A333, INTEGRA1:4;
A354: ( 1 <= i & i <= len (T . n) ) by A350, FINSEQ_1:1;
then ( 1 <= i & i + 0 <= (len (T . n)) + 1 ) by XREAL_1:7;
then A355: i in Seg ((len (T . n)) + 1) ;
( 1 + 0 <= i + 1 & i <= len (T . n) ) by A350, FINSEQ_1:1, XREAL_1:7;
then ( 1 + 0 <= i + 1 & i + 1 <= (len (T . n)) + 1 ) by XREAL_1:7;
then A356: i + 1 in Seg ((len (T . n)) + 1) ;
A357: z . i = r

proof

set f0 = [.a,b.] --> 0;
set f1 = ([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0);
set g1 = [.a,((T . n) . i).] --> 1;
set g2 = ].((T . n) . i),b.] --> 0;
set f2 = ([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0);
set h1 = [.a,((T . n) . (i - 1)).] --> 1;
set h2 = ].((T . n) . (i - 1)),b.] --> 0;
B20: ( dom ([.a,b.] --> 0) = [.a,b.] & dom ([.a,((T . n) . i).] --> 1) = [.a,((T . n) . i).] & dom (].((T . n) . i),b.] --> 0) = ].((T . n) . i),b.] & dom ([.a,((T . n) . (i - 1)).] --> 1) = [.a,((T . n) . (i - 1)).] & dom (].((T . n) . (i - 1)),b.] --> 0) = ].((T . n) . (i - 1)),b.] ) by FUNCOP_1:13;

per cases ( i = 1 or i <> 1 ) ;

suppose A358: i = 1 ; :: thesis: z . i = r

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A359: lower_bound A = a by A7, INTEGRA1:5;
A360: a in [.a,b.] by A7;
A361: (T . n) . i in [.a,b.] by A7, A332, INTEGRA1:6;
A362: ( lower_bound (divset ((T . n),i)) = lower_bound A & upper_bound (divset ((T . n),i)) = (T . n) . i ) by A332, A358, INTEGRA1:def 4;
A364: a < (T . n) . i by A264, A358;
A365: Dp1 (m,(T . n),(i + 1)) = m . ((T . n) . ((i + 1) - 1)) by A356, defDp1, A358
.= ([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) by A8, A361, A364 ;
A366: Dp1 (m,(T . n),i) = m . (lower_bound A) by A355, A358, defDp1
.= [.a,b.] --> 0 by A8, A359, A360 ;
A368: dom ([.a,b.] --> 0) = A by A7, FUNCOP_1:13;
A369: ( a <= (T . n) . i & (T . n) . i <= b ) by A361, XXREAL_1:1;
A370: dom (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) = (dom ([.a,((T . n) . i).] --> 1)) \/ (dom (].((T . n) . i),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B20, A369, XXREAL_1:167 ;
rng ([.a,b.] --> 0) c= REAL ;
then reconsider f0 = [.a,b.] --> 0 as Function of A,REAL by A368, FUNCT_2:2;
rng (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) as Function of A,REAL by A370, FUNCT_2:2;
A372: qi . t = r * ((f1 . t) - (f0 . t))

proof

reconsider H = (Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
qi = r * H by Lm1, A351, A338;
then qi . t = r * (h . t) by C0SP1:30
.= r * ((f1 . t) - (f0 . t)) by A2, A365, A366, C0SP1:34 ;
hence qi . t = r * ((f1 . t) - (f0 . t)) ; :: thesis: verum

end;

A373: t in [.a,((T . n) . i).] by A359, A362, INTEGRA1:4, A333;
then A375: f1 . t = ([.a,((T . n) . i).] --> 1) . t by FUNCT_4:16, B20, XXREAL_1:90
.= 1 by A373, FUNCOP_1:7 ;
f0 . t = 0 by A7, FUNCOP_1:7;
hence z . i = r by A351, A372, A375; :: thesis: verum

end;

suppose A376: i <> 1 ; :: thesis: z . i = r

then A378: (T . n) . (i - 1) in [.a,b.] by A7, A332, INTEGRA1:7;
A377: (T . n) . i in [.a,b.] by A7, A332, INTEGRA1:6;
A379: ( lower_bound (divset ((T . n),i)) = (T . n) . (i - 1) & upper_bound (divset ((T . n),i)) = (T . n) . i ) by A332, A376, INTEGRA1:def 4;
i - 1 in dom (T . n) by A332, A376, INTEGRA1:7;
then A382: (T . n) . (i - 1) < (T . n) . i by A332, XREAL_1:146, VALUED_0:def 13;
( (T . n) . (i - 1) = a or (T . n) . (i - 1) in ].a,b.] ) by A376, A7, A332, INTEGRA1:7, XXREAL_1:6;

per cases then ( a = (T . n) . (i - 1) or a < (T . n) . (i - 1) ) by XXREAL_1:2;

suppose A384: a = (T . n) . (i - 1) ; :: thesis: z . i = r

1 + 0 < i + 1 by XREAL_1:8, A354;
then A386: Dp1 (m,(T . n),(i + 1)) = m . ((T . n) . ((i + 1) - 1)) by A356, defDp1
.= ([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) by A8, A377, A384, A382 ;
A387: Dp1 (m,(T . n),i) = m . ((T . n) . (i - 1)) by A355, A376, defDp1
.= [.a,b.] --> 0 by A8, A378, A384 ;
A389: dom ([.a,b.] --> 0) = A by A7, FUNCOP_1:13;
A390: ( a <= (T . n) . i & (T . n) . i <= b ) by A377, XXREAL_1:1;
A392: dom (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) = (dom ([.a,((T . n) . i).] --> 1)) \/ (dom (].((T . n) . i),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B20, A390, XXREAL_1:167 ;
rng ([.a,b.] --> 0) c= REAL ;
then reconsider f0 = [.a,b.] --> 0 as Function of A,REAL by A389, FUNCT_2:2;
rng (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) as Function of A,REAL by A392, FUNCT_2:2;
A394: qi . t = r * ((f1 . t) - (f0 . t))

proof

reconsider H = (Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
qi = r * H by Lm1, A351, A338;
then qi . t = r * (h . t) by C0SP1:30
.= r * ((f1 . t) - (f0 . t)) by A2, A386, A387, C0SP1:34 ;
hence qi . t = r * ((f1 . t) - (f0 . t)) ; :: thesis: verum

end;

A395: t in [.((T . n) . (i - 1)),((T . n) . i).] by A379, INTEGRA1:4, A333;
( a <= (T . n) . (i - 1) & (T . n) . (i - 1) <= b ) by A378, XXREAL_1:1;
then B396: [.((T . n) . (i - 1)),((T . n) . i).] c= [.a,((T . n) . i).] by XXREAL_1:34;
then A398: f1 . t = ([.a,((T . n) . i).] --> 1) . t by A395, FUNCT_4:16, B20, XXREAL_1:90
.= 1 by B396, A395, FUNCOP_1:7 ;
f0 . t = 0 by A7, FUNCOP_1:7;
hence z . i = r by A351, A394, A398; :: thesis: verum

end;

suppose A399: a < (T . n) . (i - 1) ; :: thesis: z . i = r

1 + 0 < i + 1 by XREAL_1:8, A354;
then A401: Dp1 (m,(T . n),(i + 1)) = m . ((T . n) . ((i + 1) - 1)) by A356, defDp1
.= ([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) by A8, A377, A399, A382 ;
A402: Dp1 (m,(T . n),i) = m . ((T . n) . (i - 1)) by A355, A376, defDp1
.= ([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0) by A8, A378, A399 ;
A404: ( a <= (T . n) . i & (T . n) . i <= b ) by A377, XXREAL_1:1;
A405: ( a <= (T . n) . (i - 1) & (T . n) . (i - 1) <= b ) by A378, XXREAL_1:1;
A406: dom (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) = (dom ([.a,((T . n) . i).] --> 1)) \/ (dom (].((T . n) . i),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B20, A404, XXREAL_1:167 ;
A407: dom (([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0)) = (dom ([.a,((T . n) . (i - 1)).] --> 1)) \/ (dom (].((T . n) . (i - 1)),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B20, A405, XXREAL_1:167 ;
rng (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) as Function of A,REAL by A406, FUNCT_2:2;
rng (([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0)) c= REAL ;
then reconsider f2 = ([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0) as Function of A,REAL by A407, FUNCT_2:2;
A408: ( a <= t & t <= b ) by XXREAL_1:1, A7;
A409: qi . t = r * ((f1 . t) - (f2 . t))

proof

reconsider H = (Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
qi = r * H by Lm1, A351, A338;
then qi . t = r * (h . t) by C0SP1:30
.= r * ((f1 . t) - (f2 . t)) by A2, A401, A402, C0SP1:34 ;
hence qi . t = r * ((f1 . t) - (f2 . t)) ; :: thesis: verum

end;

A410: t in [.((T . n) . (i - 1)),((T . n) . i).] by A379, INTEGRA1:4, A333;
B411: [.((T . n) . (i - 1)),((T . n) . i).] c= [.a,((T . n) . i).] by A405, XXREAL_1:34;
then A413: f1 . t = ([.a,((T . n) . i).] --> 1) . t by A410, FUNCT_4:16, B20, XXREAL_1:90
.= 1 by B411, A410, FUNCOP_1:7 ;
( (T . n) . (i - 1) < t & t <= (T . n) . i ) by A332, INTEGRA1:def 4, A334, A376;
then A414: t in ].((T . n) . (i - 1)),b.] by A408;
then f2 . t = (].((T . n) . (i - 1)),b.] --> 0) . t by B20, FUNCT_4:13
.= 0 by A414, FUNCOP_1:7 ;
hence z . i = r by A351, A409, A413; :: thesis: verum

end;

end;

end;

end;

end;

for k being Nat st k in dom z & k <> i holds
z . k = 0

proof

let k be Nat; :: thesis: ( k in dom z & k <> i implies z . k = 0 )
assume that
A415: k in dom z and
A416: k <> i ; :: thesis: z . k = 0
consider r being Real such that
p2 . k in dom (u | (divset ((T . n),k))) and
r = (u | (divset ((T . n),k))) . (p2 . k) and
A420: q2 . k = r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))) by A327, A328, A349, A415;
consider qk being Function of A,REAL such that
A423: ( qk = q2 . k & z . k = qk . t ) by A344, A415;
A425: k in dom (T . n) by A344, A415, FINSEQ_1:def 3;
A426: ( 1 <= k & k <= len (T . n) ) by A344, A415, FINSEQ_1:1;
then k + 0 <= (len (T . n)) + 1 by XREAL_1:7;
then A427: k in Seg ((len (T . n)) + 1) by A426;
e: 1 + 0 <= k + 1 by XREAL_1:7;
k + 1 <= (len (T . n)) + 1 by XREAL_1:7, A426;
then A428: k + 1 in Seg ((len (T . n)) + 1) by e;
set f0 = [.a,b.] --> 0;
set f1 = ([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0);
set g1 = [.a,((T . n) . k).] --> 1;
set g2 = ].((T . n) . k),b.] --> 0;
set f2 = ([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0);
set h1 = [.a,((T . n) . (k - 1)).] --> 1;
set h2 = ].((T . n) . (k - 1)),b.] --> 0;
B30: ( dom ([.a,b.] --> 0) = [.a,b.] & dom ([.a,((T . n) . k).] --> 1) = [.a,((T . n) . k).] & dom (].((T . n) . k),b.] --> 0) = ].((T . n) . k),b.] & dom ([.a,((T . n) . (k - 1)).] --> 1) = [.a,((T . n) . (k - 1)).] & dom (].((T . n) . (k - 1)),b.] --> 0) = ].((T . n) . (k - 1)),b.] ) by FUNCOP_1:13;

per cases ( k = 1 or k <> 1 ) ;

suppose A429: k = 1 ; :: thesis: z . k = 0

then A433: ( lower_bound (divset ((T . n),i)) = (T . n) . (i - 1) & upper_bound (divset ((T . n),i)) = (T . n) . i ) by A332, INTEGRA1:def 4, A416;
A435: i - 1 in dom (T . n) by A332, A429, A416, INTEGRA1:7;
A440: (T . n) . k in [.a,b.] by A7, A425, INTEGRA1:6;
then A446: ( a <= (T . n) . k & (T . n) . k <= b ) by XXREAL_1:1;
A445: dom ([.a,b.] --> 0) = A by A7, FUNCOP_1:13;
A447: dom (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) = (dom ([.a,((T . n) . k).] --> 1)) \/ (dom (].((T . n) . k),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B30, A446, XXREAL_1:167 ;
rng ([.a,b.] --> 0) c= REAL ;
then reconsider f0 = [.a,b.] --> 0 as Function of A,REAL by A445, FUNCT_2:2;
rng (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0) as Function of A,REAL by A447, FUNCT_2:2;
A451: a < (T . n) . k by A264, A429;
A452: Dp1 (m,(T . n),(k + 1)) = m . ((T . n) . ((k + 1) - 1)) by A428, defDp1, A429
.= ([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0) by A8, A440, A451 ;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A438: lower_bound A = a by A7, INTEGRA1:5;
A439: a in [.a,b.] by A7;
A443: Dp1 (m,(T . n),k) = m . (lower_bound A) by A427, A429, defDp1
.= [.a,b.] --> 0 by A8, A438, A439 ;
A453: qk . t = r * ((f1 . t) - (f0 . t))

proof

reconsider H = (Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
qk = r * H by Lm1, A423, A420;
then qk . t = r * (h . t) by C0SP1:30
.= r * ((f1 . t) - (f0 . t)) by A2, A443, A452, C0SP1:34 ;
hence qk . t = r * ((f1 . t) - (f0 . t)) ; :: thesis: verum

end;

k < i by A429, A416, A354, XXREAL_0:1;
then k + 1 <= i by NAT_1:13;
then A456: (k + 1) - 1 <= i - 1 by XREAL_1:13;
(T . n) . k <= (T . n) . (i - 1)

proof

( k = i - 1 or k < i - 1 ) by A456, XXREAL_0:1;
hence (T . n) . k <= (T . n) . (i - 1) by A425, A435, VALUED_0:def 13; :: thesis: verum

end;

then A457: (T . n) . k < t by A334, A429, A416, XXREAL_0:2, A433;
( a <= t & t <= b ) by XXREAL_1:1, A7;
then A459: t in ].((T . n) . k),b.] by A457;
then A461: f1 . t = (].((T . n) . k),b.] --> 0) . t by B30, FUNCT_4:13
.= 0 by A459, FUNCOP_1:7 ;
f0 . t = 0 by A7, FUNCOP_1:7;
hence z . k = 0 by A423, A453, A461; :: thesis: verum

end;

suppose A462: k <> 1 ; :: thesis: z . k = 0

then A464: (T . n) . (k - 1) in [.a,b.] by A7, A425, INTEGRA1:7;
A463: (T . n) . k in [.a,b.] by A7, A425, INTEGRA1:6;
A467: k - 1 in dom (T . n) by A425, A462, INTEGRA1:7;
then A468: (T . n) . (k - 1) < (T . n) . k by A425, XREAL_1:146, VALUED_0:def 13;
1 < k by A426, A462, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A470: 2 - 1 <= k - 1 by XREAL_1:13;
1 <= len (T . n) by A426, XXREAL_0:2;
then A471: 1 in dom (T . n) by FINSEQ_3:25;
(T . n) . 1 <= (T . n) . (k - 1)

proof

( 1 = k - 1 or 1 < k - 1 ) by A470, XXREAL_0:1;
hence (T . n) . 1 <= (T . n) . (k - 1) by A467, A471, VALUED_0:def 13; :: thesis: verum

end;

then A472: a < (T . n) . (k - 1) by A264, XXREAL_0:2;
1 + 0 < k + 1 by XREAL_1:8, A426;
then A474: Dp1 (m,(T . n),(k + 1)) = m . ((T . n) . ((k + 1) - 1)) by A428, defDp1
.= ([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0) by A8, A463, A472, A468 ;
A475: Dp1 (m,(T . n),k) = m . ((T . n) . (k - 1)) by A427, A462, defDp1
.= ([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0) by A8, A464, A472 ;
A477: ( a <= (T . n) . k & (T . n) . k <= b ) by A463, XXREAL_1:1;
A478: ( a <= (T . n) . (k - 1) & (T . n) . (k - 1) <= b ) by A464, XXREAL_1:1;
A479: dom (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) = (dom ([.a,((T . n) . k).] --> 1)) \/ (dom (].((T . n) . k),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B30, A477, XXREAL_1:167 ;
A480: dom (([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0)) = (dom ([.a,((T . n) . (k - 1)).] --> 1)) \/ (dom (].((T . n) . (k - 1)),b.] --> 0)) by FUNCT_4:def 1
.= A by A7, B30, A478, XXREAL_1:167 ;
rng (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) c= REAL ;
then reconsider f1 = ([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0) as Function of A,REAL by A479, FUNCT_2:2;
rng (([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0)) c= REAL ;
then reconsider f2 = ([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0) as Function of A,REAL by A480, FUNCT_2:2;
A482: qk . t = r * ((f1 . t) - (f2 . t))

proof

reconsider H = (Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k)) as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h = H as Function of A,REAL by LM88;
qk = r * H by Lm1, A423, A420;
then qk . t = r * (h . t) by C0SP1:30
.= r * ((f1 . t) - (f2 . t)) by A2, A474, A475, C0SP1:34 ;
hence qk . t = r * ((f1 . t) - (f2 . t)) ; :: thesis: verum

end;

per cases ( i < k or k < i ) by A416, XXREAL_0:1;

suppose i < k ; :: thesis: z . k = 0

then i + 1 <= k by NAT_1:13;
then A485: (i + 1) - 1 <= k - 1 by XREAL_1:13;
A486: (T . n) . i <= (T . n) . (k - 1)

proof

( i = k - 1 or i < k - 1 ) by A485, XXREAL_0:1;
hence (T . n) . i <= (T . n) . (k - 1) by A332, A467, VALUED_0:def 13; :: thesis: verum

end;

A488: upper_bound (divset ((T . n),i)) <= (T . n) . (k - 1)

proof

per cases ( i = 1 or i <> 1 ) ;

suppose i = 1 ; :: thesis: upper_bound (divset ((T . n),i)) <= (T . n) . (k - 1)

hence upper_bound (divset ((T . n),i)) <= (T . n) . (k - 1) by A486, A332, INTEGRA1:def 4; :: thesis: verum

end;

suppose i <> 1 ; :: thesis: upper_bound (divset ((T . n),i)) <= (T . n) . (k - 1)

hence upper_bound (divset ((T . n),i)) <= (T . n) . (k - 1) by A486, A332, INTEGRA1:def 4; :: thesis: verum

end;

end;

end;

( a <= t & t <= upper_bound (divset ((T . n),i)) ) by B352, XXREAL_1:1, A7;
then A489: ( a <= t & t <= (T . n) . (k - 1) ) by A488, XXREAL_0:2;
then A490: t in [.a,((T . n) . (k - 1)).] ;
( a <= t & t <= (T . n) . k ) by A468, A489, XXREAL_0:2;
then A491: t in [.a,((T . n) . k).] ;
then A494: f1 . t = ([.a,((T . n) . k).] --> 1) . t by FUNCT_4:16, B30, XXREAL_1:90
.= 1 by A491, FUNCOP_1:7 ;
f2 . t = ([.a,((T . n) . (k - 1)).] --> 1) . t by A490, FUNCT_4:16, B30, XXREAL_1:90
.= 1 by A490, FUNCOP_1:7 ;
hence z . k = 0 by A423, A482, A494; :: thesis: verum

end;

suppose A496: k < i ; :: thesis: z . k = 0

then k + 1 <= i by NAT_1:13;
then A499: (k + 1) - 1 <= i - 1 by XREAL_1:13;
A500: i - 1 in dom (T . n) by A332, A496, A426, INTEGRA1:7;
A502: (T . n) . k <= (T . n) . (i - 1)

proof

( k = i - 1 or k < i - 1 ) by A499, XXREAL_0:1;
hence (T . n) . k <= (T . n) . (i - 1) by A425, A500, VALUED_0:def 13; :: thesis: verum

end;

(T . n) . (i - 1) < t by A496, A426, A334, A332, INTEGRA1:def 4;
then A504: (T . n) . k < t by A502, XXREAL_0:2;
then A505: (T . n) . (k - 1) < t by A468, XXREAL_0:2;
A506: ( a <= t & t <= b ) by XXREAL_1:1, A7;
then A507: t in ].((T . n) . k),b.] by A504;
then A509: f1 . t = (].((T . n) . k),b.] --> 0) . t by B30, FUNCT_4:13
.= 0 by A507, FUNCOP_1:7 ;
A508: t in ].((T . n) . (k - 1)),b.] by A505, A506;
then f2 . t = (].((T . n) . (k - 1)),b.] --> 0) . t by B30, FUNCT_4:13
.= 0 by A508, FUNCOP_1:7 ;
hence z . k = 0 by A423, A482, A509; :: thesis: verum

end;

end;

end;

end;

end;

hence g1 . t = g . (p2 . i) by A317, A336, FUNCT_1:47, A348, A337, A347, A357, INTEGR23:6; :: thesis: verum

end;

A511: for t being Element of A holds |.((g1 . t) - (g . t)).| < r / 2

proof

let t be Element of A; :: thesis: |.((g1 . t) - (g . t)).| < r / 2
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A512: lower_bound A = a by A7, INTEGRA1:5;
a < (T . n) . 1 by A264;
then consider j being Element of NAT such that
A540: j in dom (T . n) and
A541: t in divset ((T . n),j) and
A542: ( j = 1 or ( lower_bound (divset ((T . n),j)) < t & t <= upper_bound (divset ((T . n),j)) ) ) by A512, LM94;
reconsider i = j as Nat ;
set tD = p2 . i;
A543: for tD, t being Real st tD in dom g & t in dom g & |.(tD - t).| < s holds
|.((g . tD) - (g . t)).| < r / 2

proof

let tD, t be Real; :: thesis: ( tD in dom g & t in dom g & |.(tD - t).| < s implies |.((g . tD) - (g . t)).| < r / 2 )
assume A544: ( tD in dom g & t in dom g & |.(tD - t).| < s ) ; :: thesis: |.((g . tD) - (g . t)).| < r / 2
B545: dom g = dom (u | A) by A260, RELAT_1:62, A317;
then ( (u | A) . tD = u . tD & (u | A) . t = u . t ) by A544, FUNCT_1:47;
hence |.((g . tD) - (g . t)).| < r / 2 by A317, B545, A323, A544; :: thesis: verum

end;

p2 . i in dom (u | (divset ((T . n),i))) by A327, A540;
then p2 . i in (dom u) /\ (divset ((T . n),i)) by RELAT_1:61;
then A549: ( p2 . i in dom u & p2 . i in divset ((T . n),i) ) by XBOOLE_0:def 4;
then B551: |.((p2 . i) - t).| < s by A329, A540, A541, INTEGR20:12;
g1 . t = g . (p2 . i) by A331, A540, A541, A542;
hence |.((g1 . t) - (g . t)).| < r / 2 by B551, A543, A549, A260, A317; :: thesis: verum

end;

reconsider z = (xD . n) - v0 as Element of (R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider g0 = z as Function of A,REAL by LM88;
g0 in BoundedFunctions A ;
then consider g2 being Function of A,REAL such that
A552: ( g2 = g0 & g2 | A is bounded ) ;

now :: thesis: for k being Real st k in PreNorms g0 holds
k <= r / 2

let k be Real; :: thesis: ( k in PreNorms g0 implies k <= r / 2 )
assume k in PreNorms g0 ; :: thesis: k <= r / 2
then consider t being Element of A such that
A553: k = |.(g0 . t).| ;
|.((g1 . t) - (g . t)).| < r / 2 by A511;
hence k <= r / 2 by A553, A2, A317, A330, C0SP1:34; :: thesis: verum

end;

then upper_bound (PreNorms g0) <= r / 2 by SEQ_4:45;
then ||.z.|| <= r / 2 by A552, C0SP1:20;
then ||.((xD . n) - v0).|| <= r / 2 by Lm1;
hence ||.((xD . n) - v0).|| < r by A321, XXREAL_0:2; :: thesis: verum

end;

take m0 ; :: thesis: for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r
thus for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r by A325; :: thesis: verum

end;

then A555: xD is convergent by NORMSP_1:def 6;
then A556: lim xD = v by A318, NORMSP_1:def 7;
dom f = the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by FUNCT_2:def 1;
then A557: rng xD c= dom f ;
v in the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
then A558: v in dom f by FUNCT_2:def 1;
consider K being Real such that
A559: ( 0 <= K & ( for x being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) holds |.(f . x).| <= K * ||.x.|| ) ) by DUALSP01:def 9;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st x1 in dom f & ||.(x1 - v).|| < s holds
|.((f /. x1) - (f /. v)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st x1 in dom f & ||.(x1 - v).|| < s holds
|.((f /. x1) - (f /. v)).| < r ) ) )
assume A561: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st x1 in dom f & ||.(x1 - v).|| < s holds
|.((f /. x1) - (f /. v)).| < r ) )
reconsider s = r / (K + 1) as Real ;
A563: for x1 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st x1 in dom f & ||.(x1 - v).|| < s holds
|.((f /. x1) - (f /. v)).| < r

proof

let x1 be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)); :: thesis: ( x1 in dom f & ||.(x1 - v).|| < s implies |.((f /. x1) - (f /. v)).| < r )
assume that
x1 in dom f and
A565: ||.(x1 - v).|| < s ; :: thesis: |.((f /. x1) - (f /. v)).| < r
|.((f /. x1) - (f /. v)).| = |.(f . (x1 - v)).| by HAHNBAN:19;
then A567: |.((f /. x1) - (f /. v)).| <= K * ||.(x1 - v).|| by A559;
K < K + 1 by XREAL_1:145;
then A569: K * ||.(x1 - v).|| <= (K + 1) * ||.(x1 - v).|| by XREAL_1:64;
(K + 1) * ||.(x1 - v).|| < (K + 1) * s by A559, A565, XREAL_1:68;
then K * ||.(x1 - v).|| < (K + 1) * s by A569, XXREAL_0:2;
then |.((f /. x1) - (f /. v)).| < (K + 1) * s by A567, XXREAL_0:2;
hence |.((f /. x1) - (f /. v)).| < r by A559, XCMPLX_1:87; :: thesis: verum

end;

take s ; :: thesis: ( 0 < s & ( for x1 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st x1 in dom f & ||.(x1 - v).|| < s holds
|.((f /. x1) - (f /. v)).| < r ) )
thus ( 0 < s & ( for x1 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st x1 in dom f & ||.(x1 - v).|| < s holds
|.((f /. x1) - (f /. v)).| < r ) ) by A559, A561, XREAL_1:139, A563; :: thesis: verum

end;

then f is_continuous_in v by A558, NFCONT_1:8;
then f /. v = lim (f /* xD) by A555, A556, A557, NFCONT_1:def 6;
then lim (f * xD) = f . v by A557, FUNCT_2:def 11;
then f . u = integral (u,rho) by B314, FUNCT_2:def 8, A315;
hence x . u = integral (u,rho) by A6, FUNCT_1:49, A269; :: thesis: verum

end;

then B573: ||.x.|| <= total_vd rho by A251, Lm83;
take rho ; :: thesis: ( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )
thus ( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho ) by B250, A259, B573, A258, XXREAL_0:1; :: thesis: verum