dualsp05.miz



    begin

    theorem :: DUALSP05:1

    

     LM91: for d be Real holds |.( sgn d).| <= 1

    proof

      let d be Real;

      per cases ;

        suppose d > 0 ;

        then ( sgn d) = 1 by ABSVALUE:def 2;

        hence |.( sgn d).| <= 1;

      end;

        suppose d < 0 ;

        then ( sgn d) = ( - 1) by ABSVALUE:def 2;

        

        then |.( sgn d).| = ( - ( - 1)) by ABSVALUE:def 1

        .= 1;

        hence |.( sgn d).| <= 1;

      end;

        suppose d = 0 ;

        then ( sgn d) = 0 by ABSVALUE:def 2;

        hence |.( sgn d).| <= 1;

      end;

    end;

    theorem :: DUALSP05:2

    

     LM86: for x be Real holds |.x.| = (( sgn x) * x)

    proof

      let x be Real;

      

       A1: 0 < x implies |.x.| = (( sgn x) * x)

      proof

        assume

         A2: 0 < x;

        

        then (( sgn x) * x) = (1 * x) by ABSVALUE:def 2

        .= x;

        hence thesis by A2, ABSVALUE:def 1;

      end;

      

       A4: x < 0 implies |.x.| = (( sgn x) * x)

      proof

        assume

         A5: x < 0 ;

        

        then (( sgn x) * x) = (( - 1) * x) by ABSVALUE:def 2

        .= ( - x);

        hence thesis by A5, ABSVALUE:def 1;

      end;

      x = 0 implies |.x.| = (( sgn x) * x);

      hence thesis by A1, A4;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      :: DUALSP05:def1

      func ClstoCmp (A) -> strict compact non empty TopSpace means

      : Def7ClstoCmp: ex a,b be Real st a <= b & [.a, b.] = A & it = ( Closed-Interval-TSpace (a,b));

      existence

      proof

        consider a,b be Real such that

         A1: [.a, b.] = A by MEASURE5:def 3;

        consider p be object such that

         A2: p in A by XBOOLE_0:def 1;

        consider r be Real such that

         A3: r = p & a <= r & r <= b by A1, A2;

        ( Closed-Interval-TSpace (a,b)) is compact by A3, HEINE: 4, XXREAL_0: 2;

        hence thesis by A1, A3, XXREAL_0: 2;

      end;

      uniqueness

      proof

        let A1,A2 be strict compact non empty TopSpace;

        assume that

         A4: ex a,b be Real st a <= b & [.a, b.] = A & A1 = ( Closed-Interval-TSpace (a,b)) and

         A5: ex a,b be Real st a <= b & [.a, b.] = A & A2 = ( Closed-Interval-TSpace (a,b));

        consider a1,b1 be Real such that

         A6: a1 <= b1 & [.a1, b1.] = A & A1 = ( Closed-Interval-TSpace (a1,b1)) by A4;

        consider a2,b2 be Real such that

         A7: a2 <= b2 & [.a2, b2.] = A & A2 = ( Closed-Interval-TSpace (a2,b2)) by A5;

        a1 = a2 & b1 = b2 by A6, A7, XXREAL_1: 66;

        hence A1 = A2 by A6, A7;

      end;

    end

    theorem :: DUALSP05:3

    

     Th80a: for X be strict non empty SubSpace of R^1 , f be RealMap of X, g be PartFunc of REAL , REAL , x be Point of X, x0 be Real st g = f & x = x0 holds (for V be Subset of REAL st (f . x) in V & V is open holds ex W be Subset of X st x in W & W is open & (f .: W) c= V) iff g is_continuous_in x0

    proof

      let X be strict non empty SubSpace of R^1 , f be RealMap of X, g be PartFunc of REAL , REAL , x be Point of X, x0 be Real;

      assume

       AS: g = f & x = x0;

      

       A1: ( dom g) = the carrier of X by FUNCT_2:def 1, AS;

      hereby

        assume

         A2: for V be Subset of REAL st (f . x) in V & V is open holds ex W be Subset of X st x in W & W is open & (f .: W) c= V;

        for N1 be Neighbourhood of (g . x0) holds ex N be Neighbourhood of x0 st (g .: N) c= N1

        proof

          let N1 be Neighbourhood of (g . x0);

          consider s be Real such that

           A3: 0 < s & N1 = ].((g . x0) - s), ((g . x0) + s).[ by RCOMP_1:def 6;

          

           A4: ].((g . x0) - s), ((g . x0) + s).[ is open by RCOMP_1: 7;

          

           B5: |.((g . x0) - (g . x0)).| = 0 ;

          consider W be Subset of X such that

           A6: x in W & W is open & (f .: W) c= ].((g . x0) - s), ((g . x0) + s).[ by A2, A4, B5, A3, RCOMP_1: 1, AS;

          W in the topology of X by A6, PRE_TOPC:def 2;

          then

          consider W0 be Subset of R^1 such that

           A7: W0 in the topology of R^1 & W = (W0 /\ ( [#] X)) by PRE_TOPC:def 4;

          reconsider W1 = W0 as Subset of REAL ;

          W0 is open by A7, PRE_TOPC:def 2;

          then

           A8: W1 is open by BORSUK_5: 39;

          x0 in W1 by A6, A7, AS, XBOOLE_0:def 4;

          then

          consider N be Neighbourhood of x0 such that

           A9: N c= W1 by A8, RCOMP_1: 18;

          take N;

          

           A10: (g .: N) c= (g .: W1) by A9, RELAT_1: 123;

          (g .: W1) = (f .: W) by A1, A7, AS, RELAT_1: 112;

          hence (g .: N) c= N1 by A3, A6, A10;

        end;

        hence g is_continuous_in x0 by FCONT_1: 5;

      end;

      assume

       B11: g is_continuous_in x0;

      thus for V be Subset of REAL st (f . x) in V & V is open holds ex W be Subset of X st x in W & W is open & (f .: W) c= V

      proof

        let V be Subset of REAL ;

        assume (f . x) in V & V is open;

        then

        consider N1 be Neighbourhood of (f . x) such that

         A13: N1 c= V by RCOMP_1: 18;

        consider N be Neighbourhood of x0 such that

         A14: (g .: N) c= N1 by B11, FCONT_1: 5, AS;

        consider s be Real such that

         A15: 0 < s & N = ].(x0 - s), (x0 + s).[ by RCOMP_1:def 6;

        

         A16: ].(x0 - s), (x0 + s).[ is open by RCOMP_1: 7;

        

         B17: |.(x0 - x0).| = 0 ;

        reconsider W0 = ].(x0 - s), (x0 + s).[ as Subset of R^1 ;

        W0 is open by A16, BORSUK_5: 39;

        then W0 in the topology of R^1 by PRE_TOPC:def 2;

        then (W0 /\ ( [#] X)) in the topology of X by PRE_TOPC:def 4;

        then

        reconsider W = (W0 /\ ( [#] X)) as open Subset of X by PRE_TOPC:def 2;

        take W;

        x in W0 & x in ( [#] X) by B17, A15, RCOMP_1: 1, AS;

        hence x in W by XBOOLE_0:def 4;

        thus W is open;

        (f .: W) = (g .: W0) by RELAT_1: 112, A1, AS;

        hence (f .: W) c= V by A13, A14, A15;

      end;

    end;

    theorem :: DUALSP05:4

    

     Th80b: for X be strict non empty SubSpace of R^1 , f be RealMap of X, g be PartFunc of REAL , REAL st g = f holds f is continuous iff g is continuous

    proof

      let X be strict non empty SubSpace of R^1 , f be RealMap of X, g be PartFunc of REAL , REAL ;

      assume

       A1: g = f;

      

       A2: ( dom g) = the carrier of X by FUNCT_2:def 1, A1;

      hereby

        assume

         B3: f is continuous;

        for x0 be Real st x0 in ( dom g) holds g is_continuous_in x0

        proof

          let x0 be Real;

          assume x0 in ( dom g);

          then

          reconsider x = x0 as Point of X by FUNCT_2:def 1, A1;

          for V be Subset of REAL st (f . x) in V & V is open holds ex W be Subset of X st x in W & W is open & (f .: W) c= V by B3, C0SP2: 1;

          hence g is_continuous_in x0 by A1, Th80a;

        end;

        hence g is continuous by FCONT_1:def 2;

      end;

      assume

       B5: g is continuous;

      for x be Point of X holds for V be Subset of REAL st (f . x) in V & V is open holds ex W be Subset of X st x in W & W is open & (f .: W) c= V

      proof

        let x be Point of X;

        let V be Subset of REAL ;

        assume

         A6: (f . x) in V & V is open;

        reconsider x0 = x as Real;

        g is_continuous_in x0 by B5, FCONT_1:def 2, A2;

        hence ex W be Subset of X st x in W & W is open & (f .: W) c= V by A1, A6, Th80a;

      end;

      hence f is continuous by C0SP2: 1;

    end;

    theorem :: DUALSP05:5

    

     Lm1: for A be non empty closed_interval Subset of REAL holds the carrier of ( ClstoCmp A) = A

    proof

      let A be non empty closed_interval Subset of REAL ;

      consider a,b be Real such that

       A1: a <= b & [.a, b.] = A & ( ClstoCmp A) = ( Closed-Interval-TSpace (a,b)) by Def7ClstoCmp;

      thus the carrier of ( ClstoCmp A) = A by A1, TOPMETR: 10;

    end;

    theorem :: DUALSP05:6

    

     Th80: for A be non empty closed_interval Subset of REAL , u be Function holds (u is Point of ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A)) iff ( dom u) = A & u is continuous PartFunc of REAL , REAL )

    proof

      let A be non empty closed_interval Subset of REAL , u be Function;

      consider a,b be Real such that

       A1: a <= b & [.a, b.] = A & ( ClstoCmp A) = ( Closed-Interval-TSpace (a,b)) by Def7ClstoCmp;

      hereby

        assume u is Point of ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A));

        then u in ( ContinuousFunctions ( ClstoCmp A));

        then

        consider w be continuous RealMap of ( ClstoCmp A) such that

         A2: u = w;

        

         B3: ( dom w) = the carrier of ( ClstoCmp A) by FUNCT_2:def 1;

        then ( dom w) = A by Lm1;

        then ( dom w) c= REAL & ( rng w) c= REAL ;

        then

        reconsider v = w as PartFunc of REAL , REAL by RELSET_1: 4;

        v is continuous PartFunc of REAL , REAL by A1, Th80b;

        hence ( dom u) = A & u is continuous PartFunc of REAL , REAL by A2, B3, Lm1;

      end;

      assume

       A4: ( dom u) = A & u is continuous PartFunc of REAL , REAL ;

      then

       A5: ( dom u) = the carrier of ( ClstoCmp A) by Lm1;

      ( rng u) c= REAL by A4, RELAT_1:def 19;

      then

      reconsider v = u as RealMap of ( ClstoCmp A) by A5, FUNCT_2: 2;

      v is continuous by A1, A4, Th80b;

      then v in the carrier of ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A));

      hence u is Point of ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A));

    end;

    theorem :: DUALSP05:7

    

     Lm2: for A be non empty closed_interval Subset of REAL , v be Point of ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A)) holds v in ( BoundedFunctions the carrier of ( ClstoCmp A))

    proof

      let A be non empty closed_interval Subset of REAL , v be Point of ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A));

      set AV = the carrier of ( ClstoCmp A);

      ( R_Algebra_of_ContinuousFunctions ( ClstoCmp A)) is Subalgebra of ( R_Algebra_of_BoundedFunctions AV) by C0SP2: 9;

      then

       A1: the carrier of ( R_Algebra_of_ContinuousFunctions ( ClstoCmp A)) c= the carrier of ( R_Algebra_of_BoundedFunctions AV) by C0SP1:def 9;

      v in the carrier of ( R_Algebra_of_ContinuousFunctions ( ClstoCmp A));

      hence v in ( BoundedFunctions AV) by A1;

    end;

    begin

    theorem :: DUALSP05:8

    

     LM83: for A be non empty closed_interval Subset of REAL , a,b be Real st A = [.a, b.] holds ex x be Function of A, ( BoundedFunctions A) st for s be Real st s in [.a, b.] holds (s = a implies (x . s) = ( [.a, b.] --> 0 )) & (s <> a implies (x . s) = (( [.a, s.] --> 1) +* ( ].s, b.] --> 0 )))

    proof

      let A be non empty closed_interval Subset of REAL , a,b be Real;

      assume

       A2: A = [.a, b.];

      defpred C[ object] means $1 = a;

      deffunc F( object) = ( [.a, b.] --> 0 );

      deffunc G( object) = (( [.a, ( In ($1, REAL )).] --> 1) +* ( ].( In ($1, REAL )), b.] --> 0 ));

      set B = ( BoundedFunctions A);

      

       A3: for s be object st s in [.a, b.] holds ( C[s] implies F(s) in B) & ( not C[s] implies G(s) in B)

      proof

        let s be object;

        assume

         A4: s in [.a, b.];

        then

        reconsider r = s as Real;

        thus C[s] implies F(s) in B

        proof

          assume C[s];

          set f1 = ( [.a, b.] --> 0 );

          

           A7: ( dom f1) = A by A2, FUNCOP_1: 13;

          ( rng f1) c= REAL ;

          then

          reconsider f = ( [.a, b.] --> 0 ) as Function of A, REAL by A7, FUNCT_2: 2;

          reconsider r0 = 0 as Real;

          for r be ExtReal st r in ( PreNorms f) holds r <= r0

          proof

            let r be ExtReal;

            assume r in ( PreNorms f);

            then

            consider t be Element of A such that

             A8: r = |.(f . t).|;

            (f . t) = 0 by A2, FUNCOP_1: 7;

            hence r <= r0 by A8;

          end;

          then r0 is UpperBound of ( PreNorms f) by XXREAL_2:def 1;

          then ( PreNorms f) is bounded_above by XXREAL_2:def 10;

          then (f | A) is bounded by C0SP1: 18;

          hence F(s) in B;

        end;

         G(s) in B

        proof

          set g1 = ( [.a, ( In (s, REAL )).] --> 1);

          set g2 = ( ].( In (s, REAL )), b.] --> 0 );

          

           B9: a <= r & r <= b by A4, XXREAL_1: 1;

          

           A10: ( dom g1) = [.a, ( In (s, REAL )).] & ( dom g2) = ].( In (s, REAL )), b.] by FUNCOP_1: 13;

          then

           A11: (( dom g1) \/ ( dom g2)) = A by A2, B9, XXREAL_1: 167;

          then

           A12: ( dom (g1 +* g2)) = A by FUNCT_4:def 1;

          ( rng (g1 +* g2)) c= REAL ;

          then

          reconsider f = (( [.a, ( In (s, REAL )).] --> 1) +* ( ].( In (s, REAL )), b.] --> 0 )) as Function of A, REAL by A12, FUNCT_2: 2;

          reconsider r0 = 1 as Real;

          for c be object st c in (( dom g1) /\ ( dom f)) holds |.(f . c).| <= r0

          proof

            let c be object;

            assume c in (( dom g1) /\ ( dom f));

            then

             A16: c in ( dom g1) by FUNCT_4: 10, XBOOLE_1: 28;

            then |.(g1 . c).| = 1 by FUNCOP_1: 7;

            then |.((f | ( dom g1)) . c).| = 1 by FUNCT_4: 33, A10, XXREAL_1: 90;

            hence |.(f . c).| <= r0 by A16, FUNCT_1: 49;

          end;

          then

           A17: (f | ( dom g1)) is bounded by RFUNCT_1: 73;

          reconsider s0 = 0 as Real;

          for c be object st c in (( dom g2) /\ ( dom f)) holds |.(f . c).| <= s0

          proof

            let c be object;

            assume c in (( dom g2) /\ ( dom f));

            then

             A18: c in ( dom g2) by FUNCT_4: 10, XBOOLE_1: 28;

            then |.(g2 . c).| = 0 by FUNCOP_1: 7;

            then |.((f | ( dom g2)) . c).| = 0 by FUNCT_4: 23;

            hence |.(f . c).| <= s0 by A18, FUNCT_1: 49;

          end;

          then (f | ( dom g2)) is bounded by RFUNCT_1: 73;

          then (f | A) is bounded by A11, A17, RFUNCT_1: 87;

          hence G(s) in B;

        end;

        hence thesis;

      end;

      consider x be Function of [.a, b.], B such that

       A19: for s be object st s in [.a, b.] holds ( C[s] implies (x . s) = F(s)) & ( not C[s] implies (x . s) = G(s)) from FUNCT_2:sch 5( A3);

      reconsider x as Function of A, B by A2;

      take x;

      for s be Real st s in [.a, b.] holds (s = a implies (x . s) = ( [.a, b.] --> 0 )) & (s <> a implies (x . s) = (( [.a, s.] --> 1) +* ( ].s, b.] --> 0 )))

      proof

        let s be Real;

        assume

         A20: s in [.a, b.];

        ( In (s, REAL )) = s;

        hence thesis by A19, A20;

      end;

      hence thesis;

    end;

    definition

      let A be non empty closed_interval Subset of REAL , D be Division of A, m be Function of A, ( BoundedFunctions A), i be Nat;

      assume

       A1: i in ( Seg (( len D) + 1));

      :: DUALSP05:def2

      func Dp1 (m,D,i) -> Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A)) equals

      : defDp1: (m . ( lower_bound A)) if i = 1

      otherwise (m . (D . (i - 1)));

      coherence

      proof

        set V = ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A));

        hereby

          assume i = 1;

          thus (m . ( lower_bound A)) is Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A))

          proof

            set f = (m . ( lower_bound A));

            consider a,b be Real such that

             A2: a <= b & A = [.a, b.] by MEASURE5: 14;

            A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

            then

             A3: ( lower_bound A) = a by A2, INTEGRA1: 5;

            ( lower_bound A) in A by A2, A3;

            then f in ( BoundedFunctions A) by FUNCT_2: 5;

            hence thesis by Lm1;

          end;

        end;

        assume

         A5: i <> 1;

        set f = (m . (D . (i - 1)));

        

         A6: 1 <= i <= (( len D) + 1) by A1, FINSEQ_1: 1;

        then

         A7: (i - 1) <= ((( len D) + 1) - 1) by XREAL_1: 9;

        reconsider i1 = (i - 1) as Nat by A6, INT_1: 5, ORDINAL1:def 12;

        1 < i by A5, A6, XXREAL_0: 1;

        then (1 - 1) < i1 by XREAL_1: 14;

        then 1 <= i1 by NAT_1: 14;

        then (i - 1) in ( dom D) by FINSEQ_3: 25, A7;

        then f in ( BoundedFunctions A) by FUNCT_2: 5, INTEGRA1: 6;

        hence thesis by Lm1;

      end;

      correctness ;

    end

    definition

      let A be non empty closed_interval Subset of REAL , D be Division of A, rho be Function of A, REAL , i be Nat;

      :: DUALSP05:def3

      func Dp2 (rho,D,i) -> Real equals

      : defDp2: (rho . ( lower_bound A)) if i = 1

      otherwise (rho . (D . (i - 1)));

      correctness ;

    end

    theorem :: DUALSP05:9

    

     LM84: for A be non empty closed_interval Subset of REAL , D be Division of A, m be Function of A, ( BoundedFunctions A), rho be Function of A, REAL holds ex s be FinSequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A)) st ( len s) = ( len D) & for i be 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))))

    proof

      let A be non empty closed_interval Subset of REAL , D be Division of A, m be Function of A, ( BoundedFunctions A), rho be Function of A, REAL ;

      set V = ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A));

      defpred P[ Nat, set] means $2 = (( sgn (( Dp2 (rho,D,($1 + 1))) - ( Dp2 (rho,D,$1)))) * (( Dp1 (m,D,($1 + 1))) - ( Dp1 (m,D,$1))));

      

       A0: for i be Nat st i in ( Seg ( len D)) holds ex x be Element of the carrier of V st P[i, x];

      consider s be FinSequence of V such that

       A1: ( dom s) = ( Seg ( len D)) & for i be Nat st i in ( Seg ( len D)) holds P[i, (s . i)] from FINSEQ_1:sch 5( A0);

      take s;

      thus thesis by A1, FINSEQ_1:def 3;

    end;

    theorem :: DUALSP05:10

    

     LM87: for V be RealLinearSpace, f be Functional of V, s be FinSequence of V st f is additive holds (f . ( Sum s)) = ( Sum (f * s))

    proof

      let V be RealLinearSpace, f be Functional of V, s be FinSequence of V;

      assume

       A1: f is additive;

      defpred P[ Nat] means for V be RealLinearSpace, f be Functional of V, s be FinSequence of V st ( len s) = $1 & f is additive holds (f . ( Sum s)) = ( Sum (f * s));

      

       A2: P[ 0 ]

      proof

        let V be RealLinearSpace, f be Functional of V, s be FinSequence of V;

        assume that

         A3: ( len s) = 0 and

         A4: f is additive;

        

         B5: ( Sum s) = ( 0. V) by A3, RLVECT_1: 75;

        ( dom f) = the carrier of V by FUNCT_2:def 1;

        then ( rng s) c= ( dom f);

        

        then ( dom (f * s)) = ( dom s) by RELAT_1: 27

        .= ( Seg ( len s)) by FINSEQ_1:def 3;

        then ( len (f * s)) = 0 by A3, FINSEQ_1:def 3;

        then (f * s) = ( <*> REAL );

        hence thesis by B5, A4, HAHNBAN: 20, RVSUM_1: 72;

      end;

      

       A6: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A7: P[n];

        let V be RealLinearSpace, f be Functional of V, s be FinSequence of V;

        assume that

         A8: ( len s) = (n + 1) and

         A9: f is additive;

        set s0 = (s | n), p = (f * s);

        

         B10: ( dom s) = ( Seg (n + 1)) by A8, FINSEQ_1:def 3;

        then (s . (n + 1)) in ( rng s) by FUNCT_1: 3, FINSEQ_1: 4;

        then

        reconsider v = (s . (n + 1)) as Point of V;

        

         A11: n = ( len s0) by A8, FINSEQ_1: 59, NAT_1: 11;

        then

         B12: s0 = (s | ( dom s0)) by FINSEQ_1:def 3;

        

         A13: (f . (s . (n + 1))) = ((f * s) . (n + 1)) by B10, FINSEQ_1: 4, FUNCT_1: 13;

        

         A15: (f . ( Sum s)) = (f . (( Sum s0) + v)) by B12, A8, A11, RLVECT_1: 38

        .= ((f . ( Sum s0)) + (f . (s . (n + 1)))) by A9, HAHNBAN:def 2

        .= (( Sum (f * s0)) + (p . (n + 1))) by A13, A7, A9, A11;

        ( dom f) = the carrier of V by FUNCT_2:def 1;

        then ( rng s) c= ( dom f);

        

        then

         B18: ( dom (f * s)) = ( dom s) by RELAT_1: 27

        .= ( Seg ( len s)) by FINSEQ_1:def 3;

        then

         A17: ( len (f * s)) = (n + 1) by A8, FINSEQ_1:def 3;

        

         A18: 1 <= (n + 1) <= ( len p) by NAT_1: 11, B18, A8, FINSEQ_1:def 3;

        p = ((p | n) ^ <*(p /. (n + 1))*>) by A17, FINSEQ_5: 21;

        then p = ((p | n) ^ <*(p . (n + 1))*>) by A18, FINSEQ_4: 15;

        then ( Sum p) = (( Sum (p | n)) + (p . (n + 1))) by RVSUM_1: 74;

        hence thesis by A15, RELAT_1: 83;

      end;

      

       A19: for n be Nat holds P[n] from NAT_1:sch 2( A2, A6);

      ( len s) is Nat;

      hence thesis by A1, A19;

    end;

    theorem :: DUALSP05:11

    

     LM88: for A be non empty set, x be Element of ( R_Normed_Algebra_of_BoundedFunctions A) holds x is Function of A, REAL

    proof

      let A be non empty set, x be Element of ( R_Normed_Algebra_of_BoundedFunctions A);

      x is Element of ( BoundedFunctions A);

      then x is Element of ( Funcs (A, REAL ));

      hence thesis;

    end;

    theorem :: DUALSP05:12

    

     LM89: for A be non empty closed_interval Subset of REAL , s be FinSequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A)), z be FinSequence of REAL , g be Function of A, REAL , t be Element of A st ( len s) = ( len z) & g = ( Sum s) & for k be Nat st k in ( dom z) holds ex sk be Function of A, REAL st sk = (s . k) & (z . k) = (sk . t) holds (g . t) = ( Sum z)

    proof

      let A be non empty closed_interval Subset of REAL , s be FinSequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A)), z be FinSequence of REAL , g be Function of A, REAL , t be Element of A;

      assume

       A1: ( len s) = ( len z) & g = ( Sum s) & for k be Nat st k in ( dom z) holds ex sk be Function of A, REAL st sk = (s . k) & (z . k) = (sk . t);

      defpred P[ Nat] means for A be non empty closed_interval Subset of REAL , s be FinSequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A)), z be FinSequence of REAL , g be Function of A, REAL , t be Element of A st ( len s) = $1 & ( len s) = ( len z) & g = ( Sum s) & for k be Nat st k in ( dom z) holds ex sk be Function of A, REAL st sk = (s . k) & (z . k) = (sk . t) holds (g . t) = ( Sum z);

      

       A2: P[ 0 ]

      proof

        let A be non empty closed_interval Subset of REAL , s be FinSequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A)), z be FinSequence of REAL , g be Function of A, REAL , t be Element of A;

        assume that

         A3: ( len s) = 0 and

         A4: ( len s) = ( len z) and

         A5: g = ( Sum s) and for k be Nat st k in ( dom z) holds ex sk be Function of A, REAL st sk = (s . k) & (z . k) = (sk . t);

        set V = ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A));

        set AV = the carrier of ( ClstoCmp A);

        

         B8: ( Sum s) = ( 0. V) by A3, RLVECT_1: 75

        .= (AV --> 0 ) by C0SP1: 25

        .= (A --> 0 ) by Lm1;

        z = ( <*> REAL ) by A3, A4;

        hence thesis by B8, FUNCOP_1: 7, A5, RVSUM_1: 72;

      end;

      

       A9: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A10: P[n];

        let A be non empty closed_interval Subset of REAL , s be FinSequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A)), z be FinSequence of REAL , g be Function of A, REAL , t be Element of A;

        assume that

         A11: ( len s) = (n + 1) and

         A12: ( len s) = ( len z) and

         A13: g = ( Sum s) and

         A14: for k be Nat st k in ( dom z) holds ex sk be Function of A, REAL st sk = (s . k) & (z . k) = (sk . t);

        set V = ( R_Normed_Algebra_of_BoundedFunctions the carrier of ( ClstoCmp A));

        set AV = the carrier of ( ClstoCmp A);

        

         A15: A = AV by Lm1;

        set s0 = (s | n), z0 = (z | n);

        

         A16: for k be Nat st k in ( dom z0) holds ex sk be Function of A, REAL st sk = (s0 . k) & (z0 . k) = (sk . t)

        proof

          let k be Nat;

          assume k in ( dom z0);

          then

           A17: k in ( Seg n) & k in ( dom z) by RELAT_1: 57;

          then

          consider sk be Function of A, REAL such that

           A18: sk = (s . k) & (z . k) = (sk . t) by A14;

          take sk;

          thus thesis by A17, A18, FUNCT_1: 49;

        end;

        ( dom z) = ( Seg (n + 1)) by A11, A12, FINSEQ_1:def 3;

        then

        consider sk be Function of A, REAL such that

         A19: sk = (s . (n + 1)) & (z . (n + 1)) = (sk . t) by A14, FINSEQ_1: 4;

        

         A20: 1 <= (n + 1) <= ( len z) by A11, A12, NAT_1: 11;

        z = ((z | n) ^ <*(z /. (n + 1))*>) by A11, A12, FINSEQ_5: 21;

        then

         B21: z = ((z | n) ^ <*(z . (n + 1))*>) by A20, FINSEQ_4: 15;

        ( Sum s0) is Point of ( R_Normed_Algebra_of_BoundedFunctions A) by Lm1;

        then

        reconsider g1 = ( Sum s0) as Function of A, REAL by LM88;

        ( dom s) = ( Seg (n + 1)) by A11, FINSEQ_1:def 3;

        then (s . (n + 1)) in ( rng s) by FUNCT_1: 3, FINSEQ_1: 4;

        then

        reconsider v = (s . (n + 1)) as Point of V;

        v is Point of ( R_Normed_Algebra_of_BoundedFunctions A) by Lm1;

        then

        reconsider v1 = v as Function of A, REAL by LM88;

        

         A23: n = ( len s0) & n = ( len z0) by A11, A12, FINSEQ_1: 59, NAT_1: 11;

        then s0 = (s | ( dom s0)) by FINSEQ_1:def 3;

        then

         A24: ( Sum s) = (( Sum s0) + v) by A11, A23, RLVECT_1: 38;

        ( Sum s) is Point of ( R_Normed_Algebra_of_BoundedFunctions A) by Lm1;

        then

        reconsider g0 = ( Sum s) as Function of A, REAL by LM88;

        

         A25: (g0 . t) = ((g1 . t) + (sk . t)) by A19, A15, A24, C0SP1: 29;

        (g1 . t) = ( Sum z0) by A10, A16, A23;

        hence (g . t) = ( Sum z) by A13, A25, B21, A19, RVSUM_1: 74;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A9);

      hence thesis by A1;

    end;

    theorem :: DUALSP05:13

    

     LM94: for A be non empty closed_interval Subset of REAL , D be Division of A, t be Element of A st ( lower_bound A) < (D . 1) holds ex i be Element of NAT st i in ( dom D) & t in ( divset (D,i)) & (i = 1 or (( lower_bound ( divset (D,i))) < t & t <= ( upper_bound ( divset (D,i)))))

    proof

      let A be non empty closed_interval Subset of REAL , D be Division of A, t be Element of A;

      assume

       AS: ( lower_bound A) < (D . 1);

      consider i be Element of NAT such that

       A24: i in ( dom D) and

       A25: t in ( divset (D,i)) by INTEGRA3: 3;

      per cases ;

        suppose i = 1;

        hence thesis by A24, A25;

      end;

        suppose

         A26: i <> 1;

        t in [.( lower_bound ( divset (D,i))), ( upper_bound ( divset (D,i))).] by A25, INTEGRA1: 4;

        then

         A30: ( lower_bound ( divset (D,i))) <= t & t <= ( upper_bound ( divset (D,i))) by XXREAL_1: 1;

        thus ex i be Element of NAT st i in ( dom D) & t in ( divset (D,i)) & (i = 1 or (( lower_bound ( divset (D,i))) < t & t <= ( upper_bound ( divset (D,i)))))

        proof

          per cases ;

            suppose not ( lower_bound ( divset (D,i))) = t;

            then ( lower_bound ( divset (D,i))) < t by A30, XXREAL_0: 1;

            hence thesis by A24, A25, A30;

          end;

            suppose

             A31: ( lower_bound ( divset (D,i))) = t;

            

             A38: (i - 1) in ( dom D) by A24, A26, INTEGRA1: 7;

            reconsider j = (i - 1) as Element of NAT by A24, A26, INTEGRA1: 7;

            

             A40: t = ( upper_bound ( divset (D,j))) & t in ( divset (D,j))

            proof

              j = 1 or j <> 1;

              then ( upper_bound ( divset (D,j))) = (D . (i - 1)) by A38, INTEGRA1:def 4;

              hence

               A41: t = ( upper_bound ( divset (D,j))) by A31, A24, A26, INTEGRA1:def 4;

              ( lower_bound ( divset (D,j))) <= ( upper_bound ( divset (D,j))) by SEQ_4: 11;

              then t in [.( lower_bound ( divset (D,j))), ( upper_bound ( divset (D,j))).] by A41;

              hence thesis by INTEGRA1: 4;

            end;

            ( lower_bound ( divset (D,j))) < ( upper_bound ( divset (D,j)))

            proof

              per cases ;

                suppose

                 A42: j = 1;

                then ( lower_bound ( divset (D,j))) = ( lower_bound A) & ( upper_bound ( divset (D,j))) = (D . j) by A38, INTEGRA1:def 4;

                hence thesis by AS, A42;

              end;

                suppose

                 A44: j <> 1;

                then

                 A45: (( lower_bound ( divset (D,j))) = (D . (j - 1)) & ( upper_bound ( divset (D,j))) = (D . j)) by A38, INTEGRA1:def 4;

                (j - 1) in ( dom D) by A38, A44, INTEGRA1: 7;

                hence thesis by A45, A38, XREAL_1: 146, VALUED_0:def 13;

              end;

            end;

            hence thesis by A38, A40;

          end;

        end;

      end;

    end;

    

     LM95A: for A be non empty closed_interval Subset of REAL , D be Division of A st 0 < ( vol A) & (D . 1) = ( lower_bound A) holds (D /^ 1) is Division of A

    proof

      let A be non empty closed_interval Subset of REAL , D be Division of A;

      assume

       A1: 0 < ( vol A) & (D . 1) = ( lower_bound A);

       0 < ( len D);

      then

       A2: ( 0 + 1) <= ( len D) by NAT_1: 13;

      1 <> ( len D)

      proof

        assume 1 = ( len D);

        then (D . 1) = ( upper_bound A) by INTEGRA1:def 2;

        hence contradiction by A1;

      end;

      then 1 < ( len D) by A2, XXREAL_0: 1;

      then (1 + 1) <= ( len D) by NAT_1: 13;

      then

       A5: ((1 + 1) - 1) <= (( len D) - 1) by XREAL_1: 9;

      

       A6: (( len D) - 1) = ( len (D /^ 1)) by A2, RFINSEQ:def 1;

      

       A8: ( len (D /^ 1)) <> 0 by A5, RFINSEQ:def 1, A2;

      then ( len (D /^ 1)) in ( Seg ( len (D /^ 1))) by FINSEQ_1: 3;

      then

       A9: ( len (D /^ 1)) in ( dom (D /^ 1)) by FINSEQ_1:def 3;

      for e1,e2 be Nat st e1 in ( dom (D /^ 1)) & e2 in ( dom (D /^ 1)) & e1 < e2 holds ((D /^ 1) . e1) < ((D /^ 1) . e2)

      proof

        let e1,e2 be Nat;

        assume

         A10: e1 in ( dom (D /^ 1)) & e2 in ( dom (D /^ 1)) & e1 < e2;

        then

         A11: ((D /^ 1) . e1) = (D . (e1 + 1)) & ((D /^ 1) . e2) = (D . (e2 + 1)) by A2, RFINSEQ:def 1;

        1 <= e1 & e1 <= ( len (D /^ 1)) by A10, FINSEQ_3: 25;

        then (1 + 0 ) <= (e1 + 1) <= (( len (D /^ 1)) + 1) by XREAL_1: 7;

        then

         A14: (e1 + 1) in ( dom D) by A6, FINSEQ_3: 25;

        1 <= e2 <= ( len (D /^ 1)) by A10, FINSEQ_3: 25;

        then (1 + 0 ) <= (e2 + 1) & (e2 + 1) <= (( len (D /^ 1)) + 1) by XREAL_1: 7;

        then

         A15: (e2 + 1) in ( dom D) by FINSEQ_3: 25, A6;

        (e1 + 1) < (e2 + 1) by A10, XREAL_1: 8;

        hence thesis by A11, A14, A15, VALUED_0:def 13;

      end;

      then

       A16: (D /^ 1) is increasing;

      

       A17: ( len (D /^ 1)) = (( len D) - 1) by A2, RFINSEQ:def 1;

      

       B23: for x be object st x in ( rng (D /^ 1)) holds x in ( rng D)

      proof

        let x be object;

        assume x in ( rng (D /^ 1));

        then

        consider m be Nat such that

         A18: m in ( dom (D /^ 1)) and

         A19: ((D /^ 1) . m) = x by FINSEQ_2: 10;

        

         B20: m <= ( len (D /^ 1)) by A18, FINSEQ_3: 25;

        1 <= (m + 1) by NAT_1: 11;

        then

         A22: (m + 1) in ( dom D) by B20, A17, XREAL_1: 19, FINSEQ_3: 25;

        ((D /^ 1) . m) = (D . (m + 1)) by A2, A18, RFINSEQ:def 1;

        hence x in ( rng D) by A19, A22, FUNCT_1:def 3;

      end;

      ( rng D) c= A by INTEGRA1:def 2;

      then

       A24: ( rng (D /^ 1)) c= A by B23;

      

       A25: ((D /^ 1) . ( len (D /^ 1))) = (D . (( len (D /^ 1)) + 1)) by A2, A9, RFINSEQ:def 1

      .= (D . ((( len D) - 1) + 1)) by A2, RFINSEQ:def 1

      .= ( upper_bound A) by INTEGRA1:def 2;

      (D /^ 1) <> {} by A8;

      hence thesis by A16, A24, A25, INTEGRA1:def 2;

    end;

    

     LM95B: for A be non empty closed_interval Subset of REAL , D be Division of A st 0 < ( vol A) & (D . 1) = ( lower_bound A) holds ( lower_bound A) < ((D /^ 1) . 1)

    proof

      let A be non empty closed_interval Subset of REAL , D be Division of A;

      assume

       A1: 0 < ( vol A) & (D . 1) = ( lower_bound A);

       0 < ( len D);

      then

       A2: ( 0 + 1) <= ( len D) by NAT_1: 13;

      1 <> ( len D)

      proof

        assume 1 = ( len D);

        then (D . 1) = ( upper_bound A) by INTEGRA1:def 2;

        hence contradiction by A1;

      end;

      then 1 < ( len D) by A2, XXREAL_0: 1;

      then

       A4: (1 + 1) <= ( len D) by NAT_1: 13;

      then

       A5: ((1 + 1) - 1) <= (( len D) - 1) by XREAL_1: 9;

      1 <= ( len (D /^ 1)) by A5, A2, RFINSEQ:def 1;

      then 1 in ( dom (D /^ 1)) by FINSEQ_3: 25;

      then

       A9: ((D /^ 1) . 1) = (D . (1 + 1)) by A2, RFINSEQ:def 1;

      

       A10: 1 in ( dom D) by FINSEQ_3: 25, A2;

      2 in ( dom D) by A4, FINSEQ_3: 25;

      hence thesis by A1, A9, A10, VALUED_0:def 13;

    end;

    

     LM95C: for A be non empty closed_interval Subset of REAL , D,E be Division of A, rho be Function of A, REAL , K be var_volume of rho, D, L be var_volume of rho, E st 0 < ( vol A) & (D . 1) = ( lower_bound A) & E = (D /^ 1) holds ( Sum K) = ( Sum L)

    proof

      let A be non empty closed_interval Subset of REAL , D,E be Division of A, rho be Function of A, REAL , K be var_volume of rho, D, L be var_volume of rho, E;

      assume

       A1: 0 < ( vol A) & (D . 1) = ( lower_bound A) & E = (D /^ 1);

       0 < ( len D);

      then

       A4: ( 0 + 1) <= ( len D) by NAT_1: 13;

      

       A9: ( len K) = ((( len D) - 1) + 1) by INTEGR22:def 2

      .= (( len E) + 1) by A1, A4, RFINSEQ:def 1

      .= (( len <* 0 *>) + ( len E)) by FINSEQ_1: 40

      .= (( len <* 0 *>) + ( len L)) by INTEGR22:def 2;

      

       A10: ( dom K) = ( Seg (( len <* 0 *>) + ( len L))) by A9, FINSEQ_1:def 3;

      

       A11: for i be Nat st i in ( dom <* 0 *>) holds (K . i) = ( <* 0 *> . i)

      proof

        let i be Nat;

        assume i in ( dom <* 0 *>);

        then i in ( Seg ( len <* 0 *>)) by FINSEQ_1:def 3;

        then i in ( Seg 1) by FINSEQ_1: 40;

        then

         A13: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        then

         A14: i in ( dom D) by FINSEQ_3: 25, A4;

        

         A16: ( vol (( divset (D,i)),rho)) = ((rho . ( upper_bound ( divset (D,i)))) - (rho . ( lower_bound ( divset (D,i))))) by INTEGR22:def 1;

        ( lower_bound ( divset (D,i))) = ( lower_bound A) & ( upper_bound ( divset (D,i))) = ( lower_bound A) by A1, A13, A14, INTEGRA1:def 4;

        

        then (K . i) = |. 0 .| by A14, INTEGR22:def 2, A16

        .= ( <* 0 *> . i) by A13, FINSEQ_1: 40;

        hence thesis;

      end;

      for i be Nat st i in ( dom L) holds (K . (( len <* 0 *>) + i)) = (L . i)

      proof

        let i be Nat;

        assume

         a20: i in ( dom L);

        then i in ( Seg ( len L)) by FINSEQ_1:def 3;

        then i in ( Seg ( len E)) by INTEGR22:def 2;

        then

         A22: i in ( dom E) by FINSEQ_1:def 3;

        

         A26: 1 <= i & i <= ( len L) by a20, FINSEQ_3: 25;

        then (1 + 0 ) <= (i + 1) <= (( len L) + 1) by XREAL_1: 7;

        then 1 <= (i + 1) <= ( len K) by A9, FINSEQ_1: 40;

        then (i + 1) in ( Seg ( len K));

        then (i + 1) in ( Seg ( len D)) by INTEGR22:def 2;

        then

         A29: (i + 1) in ( dom D) by FINSEQ_1:def 3;

        then

         A30: (K . (i + 1)) = |.( vol (( divset (D,(i + 1))),rho)).| by INTEGR22:def 2;

        

         A31: ( vol (( divset (D,(i + 1))),rho)) = ((rho . ( upper_bound ( divset (D,(i + 1))))) - (rho . ( lower_bound ( divset (D,(i + 1)))))) by INTEGR22:def 1;

        ( upper_bound ( divset (D,(i + 1)))) = ( upper_bound ( divset (E,i))) & ( lower_bound ( divset (D,(i + 1)))) = ( lower_bound ( divset (E,i)))

        proof

          per cases ;

            suppose

             A33: i = 1;

            then

             B35: ( lower_bound ( divset (E,i))) = ( lower_bound A) & ( upper_bound ( divset (E,i))) = (E . i) by A22, INTEGRA1:def 4;

            ( lower_bound ( divset (D,(i + 1)))) = (D . ((i + 1) - 1)) & ( upper_bound ( divset (D,(i + 1)))) = (D . (i + 1)) by A29, INTEGRA1:def 4, A33;

            hence ( upper_bound ( divset (D,(i + 1)))) = ( upper_bound ( divset (E,i))) & ( lower_bound ( divset (D,(i + 1)))) = ( lower_bound ( divset (E,i))) by A33, B35, A1, A4, A22, RFINSEQ:def 1;

          end;

            suppose

             A36: i <> 1;

            then

             A37: ( lower_bound ( divset (E,i))) = (E . (i - 1)) & ( upper_bound ( divset (E,i))) = (E . i) by A22, INTEGRA1:def 4;

            1 < i by A26, A36, XXREAL_0: 1;

            then (1 + 1) <= i & i <= ( len E) by INTEGR22:def 2, A26, NAT_1: 13;

            then

             A39: ((1 + 1) - 1) <= (i - 1) & (i - 1) <= (( len E) - 0 ) by XREAL_1: 13;

            (i - 1) is Nat by A26, INT_1: 5, ORDINAL1:def 12;

            then (i - 1) in ( dom E) by FINSEQ_3: 25, A39;

            then

             A42: ( lower_bound ( divset (E,i))) = (D . ((i - 1) + 1)) & ( upper_bound ( divset (E,i))) = (D . (i + 1)) by A1, A4, A22, A37, RFINSEQ:def 1;

            (1 + 0 ) < (i + 1) by A26, XREAL_1: 8;

            then ( lower_bound ( divset (D,(i + 1)))) = (D . ((i + 1) - 1)) & ( upper_bound ( divset (D,(i + 1)))) = (D . (i + 1)) by A29, INTEGRA1:def 4;

            hence ( upper_bound ( divset (D,(i + 1)))) = ( upper_bound ( divset (E,i))) & ( lower_bound ( divset (D,(i + 1)))) = ( lower_bound ( divset (E,i))) by A42;

          end;

        end;

        then ( vol (( divset (D,(i + 1))),rho)) = ( vol (( divset (E,i)),rho)) by INTEGR22:def 1, A31;

        then (K . (i + 1)) = (L . i) by A22, INTEGR22:def 2, A30;

        hence thesis by FINSEQ_1: 40;

      end;

      then K = ( <* 0 *> ^ L) by A10, A11, FINSEQ_1:def 7;

      

      hence ( Sum K) = ( 0 + ( Sum L)) by RVSUM_1: 76

      .= ( Sum L);

    end;

    theorem :: DUALSP05:14

    

     LM95: for A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , B be Real st 0 < ( vol A) holds (for D be Division of A, K be var_volume of rho, D st ( lower_bound A) < (D . 1) holds ( Sum K) <= B) implies (for D be Division of A, K be var_volume of rho, D holds ( Sum K) <= B)

    proof

      let A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , B be Real;

      assume

       A1: 0 < ( vol A);

      assume

       A2: for D be Division of A, K be var_volume of rho, D st ( lower_bound A) < (D . 1) holds ( Sum K) <= B;

      let D be Division of A, K be var_volume of rho, D;

      1 <= ( len D) by FINSEQ_1: 20;

      then 1 in ( dom D) by FINSEQ_3: 25;

      then (D . 1) in A by INTEGRA1: 6;

      then ( lower_bound A) <= (D . 1) by SEQ_4:def 2;

      per cases by XXREAL_0: 1;

        suppose ( lower_bound A) < (D . 1);

        hence ( Sum K) <= B by A2;

      end;

        suppose

         A5: ( lower_bound A) = (D . 1);

        then

        reconsider E = (D /^ 1) as Division of A by A1, LM95A;

        

         A6: ( lower_bound A) < (E . 1) by A1, A5, LM95B;

        set L = the var_volume of rho, E;

        ( Sum L) <= B by A2, A6;

        hence ( Sum K) <= B by A1, A5, LM95C;

      end;

    end;

    begin

    theorem :: DUALSP05:15

    

     Lm83: for A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , f be Point of ( DualSp ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A))) st rho is bounded_variation & (for u be continuous PartFunc of REAL , REAL st ( dom u) = A holds (f . u) = ( integral (u,rho))) holds ||.f.|| <= ( total_vd rho)

    proof

      let A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , f be Point of ( DualSp ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A)));

      assume that

       A1: rho is bounded_variation and

       A2: for u be continuous PartFunc of REAL , REAL st ( dom u) = A holds (f . u) = ( integral (u,rho));

      set X = ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A));

      

       A3: for u be continuous PartFunc of REAL , REAL st u in the carrier of X holds (f . u) = ( integral (u,rho))

      proof

        let u be continuous PartFunc of REAL , REAL ;

        assume u in the carrier of X;

        then ( dom u) = A & u is continuous PartFunc of REAL , REAL by Th80;

        hence (f . u) = ( integral (u,rho)) by A2;

      end;

      

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

      proof

        let u be continuous PartFunc of REAL , REAL , v be Point of X;

        assume

         A5: ( dom u) = A & u = v;

        then

         B6: u is_RiemannStieltjes_integrable_with rho by A1, INTEGR23: 21;

        consider T be 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 S).| is convergent by SEQ_4: 13, B6, A7;

        

         A10: for n be Nat holds |.(( middle_sum S) . n).| <= ( ||.v.|| * ( total_vd rho))

        proof

          let n be Nat;

          set F = the var_volume of rho, (T . n);

          reconsider v0 = ||.v.|| as Real;

          reconsider vF = (v0 * F) as FinSequence of REAL ;

          ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

          then

           B14: ( dom vF) = ( Seg ( len F)) by VALUED_1:def 5;

          

           A15: ( len (S . n)) = ( len (T . n)) by A1, A5, INTEGR22:def 5

          .= ( len F) by INTEGR22:def 2

          .= ( len vF) by B14, FINSEQ_1:def 3;

          for j be Nat st j in ( dom (S . n)) holds |.((S . n) . j).| <= (vF . j)

          proof

            let j be Nat;

            assume j in ( dom (S . n));

            then

             B17: j in ( Seg ( len (S . 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 be Real such that

             A18: r in ( rng (u | ( divset ((T . n),j)))) and

             A19: ((S . n) . j) = (r * ( vol (( divset ((T . n),j)),rho))) by A1, A5, INTEGR22:def 5, A16;

            

             A20: |.((S . n) . j).| = ( |.r.| * |.( vol (( divset ((T . n),j)),rho)).|) by COMPLEX1: 65, A19

            .= ( |.r.| * (F . j)) by A16, INTEGR22:def 2;

            consider x be 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 AV) by A5, Lm2;

            then

            consider u1 be Function of AV, REAL such that

             A23: u = u1 & (u1 | AV) is bounded;

            x in A by A5, A21, RELAT_1: 57;

            then

            reconsider x1 = x as Element of AV by Lm1;

            reconsider v1 = v as Point of ( R_Normed_Algebra_of_BoundedFunctions AV) 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 F)) by INTEGR22:def 2;

            then j in ( dom F) by FINSEQ_1:def 3;

            then 0 <= (F . j) by INTEGR22: 3;

            then ( |.r.| * (F . j)) <= (v0 * (F . j)) by A24, XREAL_1: 64;

            hence |.((S . n) . j).| <= (vF . j) by A20, VALUED_1: 6;

          end;

          then |.( Sum (S . n)).| <= ( Sum vF) by A15, INTEGR23: 3;

          then

           A25: |.( Sum (S . n)).| <= ( ||.v.|| * ( Sum F)) by RVSUM_1: 87;

          ( ||.v.|| * ( Sum F)) <= ( ||.v.|| * ( total_vd rho)) by A1, INTEGR22: 5, XREAL_1: 64;

          then |.( Sum (S . n)).| <= ( ||.v.|| * ( total_vd rho)) by A25, XXREAL_0: 2;

          hence thesis by INTEGR22:def 7;

        end;

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

        now

          let n be Nat;

           |.(( middle_sum S) . n).| <= a by A10;

          then ( |.( middle_sum S).| . n) <= a by SEQ_1: 12;

          hence ( |.( middle_sum S).| . n) <= (( seq_const a) . n) by SEQ_1: 57;

        end;

        then ( lim |.( middle_sum S).|) <= ( lim ( seq_const a)) by A9, SEQ_2: 18;

        then

         A27: |.( lim ( middle_sum S)).| <= ( 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 thesis by B6, A1, A5, INTEGR22:def 9, A7, A27;

      end;

      reconsider g = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;

      now

        let k be Real;

        assume k in ( PreNorms g);

        then

        consider u be Point of X such that

         A28: k = |.(g . u).| & ||.u.|| <= 1;

        u in ( ContinuousFunctions ( ClstoCmp A));

        then ex v be 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 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;

      end;

      then ( upper_bound ( PreNorms g)) <= ( total_vd rho) by SEQ_4: 45;

      hence ||.f.|| <= ( total_vd rho) by DUALSP01: 24;

    end;

    theorem :: DUALSP05:16

    for A be non empty closed_interval Subset of REAL , x be Point of ( DualSp ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A))) st 0 < ( vol A) holds ex rho be Function of A, REAL st rho is bounded_variation & (for u be continuous PartFunc of REAL , REAL st ( dom u) = A holds (x . u) = ( integral (u,rho))) & ||.x.|| = ( total_vd rho)

    proof

      let A be non empty closed_interval Subset of REAL , x be Point of ( DualSp ( R_Normed_Algebra_of_ContinuousFunctions ( ClstoCmp A)));

      assume

       A1: 0 < ( vol A);

      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: AV = A by Lm1;

      ( R_Algebra_of_ContinuousFunctions ( ClstoCmp A)) is Subalgebra of ( R_Algebra_of_BoundedFunctions AV) by C0SP2: 9;

      then

       A3: the carrier of X c= the carrier of V & the addF of X = (the addF of V || the carrier of X) & the Mult of X = (the Mult of V | [: REAL , the carrier of X:]) by C0SP1:def 9;

      

       A4: ( 0. X) = (( ClstoCmp A) --> 0 ) by C0SP2: 12

      .= ( 0. V) by C0SP1: 25;

      

       B5: X is SubRealNormSpace of V by A3, A4, DUALSP01:def 16;

      reconsider h = x as Lipschitzian linear-Functional of X by DUALSP01:def 10;

      consider f be Lipschitzian linear-Functional of V, F be Point of ( DualSp V) such that

       A6: f = F & (f | the carrier of X) = h & ||.F.|| = ||.x.|| by B5, DUALSP01: 36;

      consider a,b be Real such that

       A7: a <= b & [.a, b.] = A & ( ClstoCmp A) = ( Closed-Interval-TSpace (a,b)) by Def7ClstoCmp;

      consider m be Function of A, ( BoundedFunctions A) such that

       A8: for s be 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 V = ( BoundedFunctions A) by Lm1;

      then

      reconsider rho = (f * m) as Function of A, REAL ;

      

       A9: for D be Division of A, K be var_volume of rho, D st a < (D . 1) holds ( Sum K) <= ||.x.||

      proof

        let D be Division of A, K be var_volume of rho, D;

        assume

         A10: a < (D . 1);

        consider s be FinSequence of V such that

         A11: ( len s) = ( len D) and

         A12: for i be 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);

        yD in the carrier of V;

        then yD in ( BoundedFunctions A) by Lm1;

        then

        consider g be Function of A, REAL such that

         A13: g = yD & (g | A) is bounded;

        

         A14: (f . yD) = ( Sum (f * s)) by LM87;

        

         A15: for t be Element of A holds |.(g . t).| <= 1

        proof

          let t be Element of A;

          defpred R1[ Nat, set] means ex sk be Function of A, REAL st sk = (s . $1) & $2 = (sk . t);

          

           A16: for k be Nat st k in ( Seg ( len D)) holds ex x be Element of REAL st R1[k, x]

          proof

            let k be Nat;

            assume k in ( Seg ( len D));

            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 V;

            then (s . k) in ( BoundedFunctions A) by Lm1;

            then

            consider sk be Function of A, REAL such that

             A17: sk = (s . k) & (sk | A) is bounded;

            take x = (sk . t);

            thus thesis by A17;

          end;

          consider z be FinSequence of REAL such that

           A18: ( dom z) = ( Seg ( len D)) & for k be Nat st k in ( Seg ( len D)) holds R1[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 be 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 as Nat;

          

           A54: i in ( Seg ( len D)) by A50, FINSEQ_1:def 3;

          then

          consider si be 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 <= ( 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) = r

          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 f0) = [.a, b.] & ( dom g1) = [.a, (D . i).] & ( dom g2) = ].(D . i), b.] & ( dom h1) = [.a, (D . (i - 1)).] & ( dom h2) = ].(D . (i - 1)), b.] by FUNCOP_1: 13;

            per cases ;

              suppose

               A62: i = 1;

              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 f0) = A by A7, FUNCOP_1: 13;

              

               A73: a <= (D . i) & (D . i) <= b by A65, XXREAL_1: 1;

              

               A74: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

              .= A by A7, B0, A73, XXREAL_1: 167;

              ( rng f0) c= REAL ;

              then

              reconsider f0 as Function of A, REAL by A72, FUNCT_2: 2;

              ( rng f1) c= REAL ;

              then

              reconsider f1 as Function of A, REAL by A74, FUNCT_2: 2;

              

               A76: (si . t) = (r * ((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 = (r * (( Dp1 (m,D,(i + 1))) - ( Dp1 (m,D,i)))) by A55, B56, A12;

                then si = (r * H) by Lm1;

                

                then (si . t) = (r * (h . t)) by C0SP1: 30

                .= (r * ((f1 . t) - (f0 . t))) by A2, A69, A70, C0SP1: 34;

                hence thesis;

              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 thesis by A55, A76, A79;

            end;

              suppose

               A80: i <> 1;

              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 by XXREAL_1: 2;

                suppose

                 A88: a = (D . (i - 1));

                (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 f0) = A by A7, FUNCOP_1: 13;

                

                 A94: a <= (D . i) & (D . i) <= b by A81, XXREAL_1: 1;

                

                 A96: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

                .= A by A7, B0, A94, XXREAL_1: 167;

                ( rng f0) c= REAL ;

                then

                reconsider f0 as Function of A, REAL by A93, FUNCT_2: 2;

                ( rng f1) c= REAL ;

                then

                reconsider f1 as Function of A, REAL by A96, FUNCT_2: 2;

                

                 A98: (si . t) = (r * ((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 = (r * (( Dp1 (m,D,(i + 1))) - ( Dp1 (m,D,i)))) by A55, B56, A12;

                  then si = (r * H) by Lm1;

                  

                  then (si . t) = (r * (h . t)) by C0SP1: 30

                  .= (r * ((f1 . t) - (f0 . t))) by A2, A90, A91, C0SP1: 34;

                  hence thesis;

                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 thesis by A55, A98, A102;

              end;

                suppose

                 A103: a < (D . (i - 1));

                (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) <= b by A81, XXREAL_1: 1;

                

                 A109: a <= (D . (i - 1)) <= b by A82, XXREAL_1: 1;

                

                 A110: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

                .= A by A7, B0, A108, XXREAL_1: 167;

                

                 A111: ( dom f2) = (( dom h1) \/ ( dom h2)) by FUNCT_4:def 1

                .= A by A7, B0, A109, XXREAL_1: 167;

                ( rng f1) c= REAL ;

                then

                reconsider f1 as Function of A, REAL by A110, FUNCT_2: 2;

                ( rng f2) c= REAL ;

                then

                reconsider f2 as Function of A, REAL by A111, FUNCT_2: 2;

                

                 A112: a <= t & t <= b by XXREAL_1: 1, A7;

                

                 A113: (si . t) = (r * ((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 = (r * (( Dp1 (m,D,(i + 1))) - ( Dp1 (m,D,i)))) by A55, B56, A12;

                  then si = (r * H) by Lm1;

                  

                  then (si . t) = (r * (h . t)) by C0SP1: 30

                  .= (r * ((f1 . t) - (f2 . t))) by A2, A105, A106, C0SP1: 34;

                  hence thesis;

                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 thesis by A55, A113, A117;

              end;

            end;

          end;

          then

           A119: |.(z . i).| <= 1 by LM91;

          for k be Nat st k in ( dom z) & k <> i holds (z . k) = 0

          proof

            let k be Nat;

            assume that

             A120: k in ( dom z) and

             A121: k <> i;

            consider sk be 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 <= ( 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 f0) = [.a, b.] & ( dom g1) = [.a, (D . k).] & ( dom g2) = ].(D . k), b.] & ( dom h1) = [.a, (D . (k - 1)).] & ( dom h2) = ].(D . (k - 1)), b.] by FUNCOP_1: 13;

            per cases ;

              suppose

               A130: k = 1;

              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 f0) = A by A7, FUNCOP_1: 13;

              

               A148: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

              .= A by A7, B10, A147, XXREAL_1: 167;

              ( rng f0) c= REAL ;

              then

              reconsider f0 as Function of A, REAL by A146, FUNCT_2: 2;

              ( rng f1) c= REAL ;

              then

              reconsider f1 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) = (r * ((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 = (r * (( Dp1 (m,D,(k + 1))) - ( Dp1 (m,D,k)))) by A124, B125, A12;

                then sk = (r * H) by Lm1;

                

                then (sk . t) = (r * (h . t)) by C0SP1: 30

                .= (r * ((f1 . t) - (f0 . t))) by A2, A144, A153, C0SP1: 34;

                hence thesis;

              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 thesis by A126, A136, VALUED_0:def 13;

              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 thesis by A124, A154, A162;

            end;

              suppose

               A163: k <> 1;

              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 thesis by A168, A172, VALUED_0:def 13;

              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 f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

              .= A by A7, B10, A178, XXREAL_1: 167;

              

               A181: ( dom f2) = (( dom h1) \/ ( dom h2)) by FUNCT_4:def 1

              .= A by A7, B10, A179, XXREAL_1: 167;

              ( rng f1) c= REAL ;

              then

              reconsider f1 as Function of A, REAL by A180, FUNCT_2: 2;

              ( rng f2) c= REAL ;

              then

              reconsider f2 as Function of A, REAL by A181, FUNCT_2: 2;

              

               A183: (sk . t) = (r * ((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 = (r * H) by Lm1, A124, A125;

                

                then (sk . t) = (r * (h . t)) by C0SP1: 30

                .= (r * ((f1 . t) - (f2 . t))) by A2, A175, A176, C0SP1: 34;

                hence thesis;

              end;

              per cases by A121, XXREAL_0: 1;

                suppose i < k;

                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 thesis by A50, A168, VALUED_0:def 13;

                end;

                

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

                proof

                  per cases ;

                    suppose i = 1;

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

                  end;

                    suppose i <> 1;

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

                  end;

                end;

                

                 A191: a <= t <= (D . (k - 1)) by A189, XXREAL_0: 2, A53, XXREAL_1: 1, A7;

                then

                 A192: t in [.a, (D . (k - 1)).];

                a <= 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 thesis by A124, A183, A196;

              end;

                suppose

                 A198: k < i;

                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 thesis by A126, A202, VALUED_0:def 13;

                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 thesis by A124, A183, A211;

              end;

            end;

          end;

          then |.( Sum z).| <= 1 by A22, A50, A119, INTEGR23: 6;

          hence |.(g . t).| <= 1 by A13, A20, LM89, A18;

        end;

        now

          let k be Real;

          assume k in ( PreNorms g);

          then

          consider t be Element of A such that

           A213: k = |.(g . t).|;

          thus k <= 1 by A15, A213;

        end;

        then ( upper_bound ( PreNorms g)) <= 1 by SEQ_4: 45;

        then (( BoundedFunctionsNorm A) . g) <= 1 by A13, C0SP1: 20;

        then

         A214: ||.yD.|| <= 1 by A13, Lm1;

        

         A215: ( len K) = ( len D) & for i be Nat st i in ( dom D) holds (K . i) = |.( vol (( divset (D,i)),rho)).| by INTEGR22:def 2;

        ( dom f) = the carrier of V 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 be Nat st i in ( dom D) holds ((f * s) . i) = |.( vol (( divset (D,i)),rho)).|

        proof

          let i be Nat;

          assume

           A218: i in ( dom D);

          then

           A220: 1 <= 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 ;

            suppose

             A227: i = 1;

            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 . (r * (( Dp1 (m,D,(i + 1))) - ( Dp1 (m,D,i))))) by A12, A223

            .= (r * (f . (( Dp1 (m,D,(i + 1))) - ( Dp1 (m,D,i))))) by HAHNBAN:def 3

            .= (r * ((f . ( Dp1 (m,D,(i + 1)))) - (f . ( Dp1 (m,D,i))))) by HAHNBAN: 19

            .= (r * ((f . (m . (D . i))) - (f . (m . ( lower_bound A))))) by A229, A221, A227, defDp1

            .= (r * (((f * m) . (D . i)) - (f . (m . ( lower_bound A))))) by A225, FUNCT_1: 13

            .= (r * ((rho . ( upper_bound ( divset (D,i)))) - (rho . ( lower_bound ( divset (D,i)))))) by A228, A226, FUNCT_1: 13

            .= (r * ( 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));

            r = ( 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;

          end;

            suppose

             A234: i <> 1;

            (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 . (r * (( Dp1 (m,D,(i + 1))) - ( Dp1 (m,D,i))))) by A12, A223

            .= (r * (f . (( Dp1 (m,D,(i + 1))) - ( Dp1 (m,D,i))))) by HAHNBAN:def 3

            .= (r * ((f . ( Dp1 (m,D,(i + 1)))) - (f . ( Dp1 (m,D,i))))) by HAHNBAN: 19

            .= (r * ((f . (m . (D . i))) - (f . (m . (D . (i - 1)))))) by A239, A221, A234, defDp1

            .= (r * (((f * m) . (D . i)) - (f . (m . (D . (i - 1)))))) by A235, FUNCT_1: 13

            .= (r * ((rho . ( upper_bound ( divset (D,i)))) - (rho . ( lower_bound ( divset (D,i)))))) by A237, A236, FUNCT_1: 13

            .= (r * ( 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));

            r = ( 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;

          end;

        end;

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

        proof

          let i be Nat;

          assume i in ( dom K);

          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 thesis by A217, A244;

        end;

        then

         A245: (f . yD) = ( Sum K) by A14, A216, FINSEQ_1: 13;

        

         A246: (f . yD) <= |.(f . yD).| by ABSVALUE: 4;

        

         A247: |.(f . yD).| <= ( ||.F.|| * ||.yD.||) by A6, DUALSP01: 26;

        ( ||.F.|| * ||.yD.||) <= ( ||.F.|| * 1) by A214, XREAL_1: 64;

        then |.(f . yD).| <= ||.F.|| by A247, XXREAL_0: 2;

        hence ( Sum K) <= ||.x.|| by A6, A245, A246, XXREAL_0: 2;

      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 be Division of A, K be var_volume of rho, D holds ( Sum K) <= ||.x.|| by A1, A9, LM95;

      then

       B250: for t be Division of A, F0 be var_volume of rho, t holds ( Sum F0) <= d by XREAL_1: 39;

      then

       A251: rho is bounded_variation;

      then

      consider VD be non empty Subset of REAL such that VD is bounded_above and

       A253: VD = { r where r be Real : ex t be Division of A, F0 be var_volume of rho, t st r = ( Sum F0) } and

       A254: ( total_vd rho) = ( upper_bound VD) by INTEGR22:def 4;

      now

        let k be Real;

        assume k in VD;

        then

        consider r be Real such that

         A255: k = r and

         A256: ex t be Division of A, F0 be var_volume of rho, t st r = ( Sum F0) by A253;

        consider t be Division of A, F0 be var_volume of rho, t such that

         A257: r = ( Sum F0) by A256;

        thus k <= ||.x.|| by A249, A1, A9, LM95, A255, A257;

      end;

      then

       A258: ( total_vd rho) <= ||.x.|| by A254, SEQ_4: 45;

      

       A259: for u be continuous PartFunc of REAL , REAL st ( dom u) = A holds (x . u) = ( integral (u,rho))

      proof

        let u be continuous PartFunc of REAL , REAL ;

        assume

         A260: ( dom u) = A;

        then

         A261: for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be 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 be DivSequence of A such that

         A263: ( delta T) is convergent & ( lim ( delta T)) = 0 & (for n be Element of NAT holds ex Tn be Division of A st (Tn divide_into_equal (n + 1) & (T . n) = Tn)) by A1, INTEGRA6: 16;

        

         A264: for n be Nat holds a < ((T . n) . 1)

        proof

          let n be Nat;

          n is Element of NAT by ORDINAL1:def 12;

          then

          consider Tn be 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) <= ( 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 thesis by A265, A249, B268, INTEGRA4:def 1;

        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 P[ Element of NAT , set] means ex p be FinSequence of REAL st p = $2 & ( len p) = ( len (T . $1)) & for i be Nat st i in ( dom (T . $1)) holds (p . i) in ( dom (u | ( divset ((T . $1),i)))) & ex z be Real st z = ((u | ( divset ((T . $1),i))) . (p . i)) & ((S . $1) . i) = (z * ( vol (( divset ((T . $1),i)),rho)));

        

         A270: for k be Element of NAT holds ex p be Element of ( REAL * ) st P[k, p]

        proof

          let k be Element of NAT ;

          defpred P1[ Nat, set] means $2 in ( dom (u | ( divset ((T . k),$1)))) & ex c be Real st c = ((u | ( divset ((T . k),$1))) . $2) & ((S . 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 be Nat st i in ( Seg ( len (T . k))) holds ex x be Element of REAL st P1[i, x]

          proof

            let i be Nat;

            assume i in ( Seg ( len (T . k)));

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

            then

            consider c be Real such that

             A273: c in ( rng (u | ( divset ((T . k),i)))) & ((S . k) . i) = (c * ( vol (( divset ((T . k),i)),rho))) by A251, A260, INTEGR22:def 5;

            consider x be 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 as Element of REAL by A274;

            take x;

            thus thesis by A273, A274;

          end;

          consider p be FinSequence of REAL such that

           A275: ( dom p) = ( Seg ( len (T . k))) & for i be Nat st i in ( Seg ( len (T . k))) holds P1[i, (p . i)] from FINSEQ_1:sch 5( A272);

          take p;

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

          hence thesis by A271, A275, FINSEQ_1:def 11;

        end;

        consider F be sequence of ( REAL * ) such that

         A276: for x be Element of NAT holds P[x, (F . x)] from FUNCT_2:sch 3( A270);

        defpred Q[ Element of NAT , object] means ex q be FinSequence of V st ( len q) = ( len (T . $1)) & $2 = ( Sum q) & for i be Nat st i in ( dom (T . $1)) holds ex r be 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 be Element of NAT holds ex x be Element of the carrier of V st Q[k, x]

        proof

          let k be Element of NAT ;

          defpred Q1[ Nat, object] means ex r be 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 be Nat st i in ( Seg ( len (T . k))) holds ex y be Element of the carrier of V st Q1[i, y]

          proof

            let i be Nat;

            assume i in ( Seg ( len (T . k)));

            then

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

            consider p be FinSequence of REAL such that

             A280: p = (F . k) & ( len p) = ( len (T . k)) & for i be Nat st i in ( dom (T . k)) holds (p . i) in ( dom (u | ( divset ((T . k),i)))) & ex z be Real st z = ((u | ( divset ((T . k),i))) . (p . i)) & ((S . 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 V;

            hence thesis by A280, A279;

          end;

          consider q be FinSequence of V such that

           A282: ( dom q) = ( Seg ( len (T . k))) & for i be Nat st i in ( Seg ( len (T . k))) holds Q1[i, (q . i)] from FINSEQ_1:sch 5( A278);

          take x = ( Sum q);

          

           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 thesis by A282, A283;

        end;

        consider xD be sequence of V such that

         A284: for z be Element of NAT holds Q[z, (xD . z)] from FUNCT_2:sch 3( A277);

        

         B314: for n be Element of NAT holds ((f * xD) . n) = (( middle_sum S) . n)

        proof

          let n be Element of NAT ;

          consider p1 be FinSequence of REAL such that

           A285: p1 = (F . n) & ( len p1) = ( len (T . n)) & for i be Nat st i in ( dom (T . n)) holds (p1 . i) in ( dom (u | ( divset ((T . n),i)))) & ex z be Real st z = ((u | ( divset ((T . n),i))) . (p1 . i)) & ((S . n) . i) = (z * ( vol (( divset ((T . n),i)),rho))) by A276;

          consider q1 be FinSequence of V such that

           A286: ( len q1) = ( len (T . n)) & (xD . n) = ( Sum q1) & for i be Nat st i in ( dom (T . n)) holds ex r be 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 S) . n) = ( Sum (S . 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 V 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 (S . n))) by A251, A260, A286, INTEGR22:def 5;

          then

           A289: ( len (f * q1)) = ( len (S . n)) by FINSEQ_1:def 3;

          for k be Nat st 1 <= k & k <= ( len (S . n)) holds ((f * q1) . k) = ((S . n) . k)

          proof

            let k be Nat;

            assume

             A290: 1 <= k & k <= ( len (S . n));

            then

             B291: k in ( Seg ( len (S . 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 be Real such that

             A293: z = ((u | ( divset ((T . n),k))) . ((F . n) . k)) & ((S . n) . k) = (z * ( vol (( divset ((T . n),k)),rho))) by A285;

            consider r be 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 <= ( 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 ;

              suppose

               A299: k = 1;

              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

              .= ((S . n) . k) by A293, A294, A306, HAHNBAN:def 3;

            end;

              suppose

               A307: k <> 1;

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

              .= ((S . n) . k) by A293, A294, A313, HAHNBAN:def 3;

            end;

          end;

          hence thesis by A287, A288, A289, FINSEQ_1: 14;

        end;

        

         A315: ( middle_sum S) is convergent & ( lim ( middle_sum S)) = ( 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 V by A269, Lm2;

        v in ( BoundedFunctions A) by A316, Lm1;

        then

        consider g be Function of A, REAL such that

         A317: g = v & (g | A) is bounded;

        reconsider v0 = v as Point of V;

        

         A318: for r be Real st 0 < r holds ex m0 be Nat st for n be Nat st m0 <= n holds ||.((xD . n) - v0).|| < r

        proof

          let r be Real;

          assume

           A319: 0 < r;

          then

           A321: (r / 2) < r by XREAL_1: 216;

          consider s be Real such that

           A322: 0 < s and

           A323: for x1,x2 be 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 be Nat such that

           A324: for i be Nat st m0 <= i holds |.((( delta T) . i) - 0 ).| < s by A263, A322, SEQ_2:def 7;

          

           A325: for n be Nat st m0 <= n holds ||.((xD . n) - v0).|| < r

          proof

            let n be Nat;

            

             A326: n in NAT by ORDINAL1:def 12;

            consider p2 be FinSequence of REAL such that

             A327: p2 = (F . n) & ( len p2) = ( len (T . n)) & for i be Nat st i in ( dom (T . n)) holds (p2 . i) in ( dom (u | ( divset ((T . n),i)))) & ex z be Real st z = ((u | ( divset ((T . n),i))) . (p2 . i)) & ((S . n) . i) = (z * ( vol (( divset ((T . n),i)),rho))) by A276, A326;

            consider q2 be FinSequence of V such that

             A328: ( len q2) = ( len (T . n)) & (xD . n) = ( Sum q2) & for i be Nat st i in ( dom (T . n)) holds ex r be 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;

            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 V;

            then (xD . n) in ( BoundedFunctions A) by Lm1;

            then

            consider g1 be Function of A, REAL such that

             A330: g1 = (xD . n) & (g1 | A) is bounded;

            

             A331: for t be Element of A, i be 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, i be Nat;

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

              consider r be 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 R2[ Nat, set] means ex qi be Function of A, REAL st qi = (q2 . $1) & $2 = (qi . t);

              

               A340: for i be Nat st i in ( Seg ( len (T . n))) holds ex x be Element of REAL st R2[i, x]

              proof

                let i be Nat;

                assume i in ( Seg ( len (T . n)));

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

                then

                consider r be 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 V by A342;

                then (q2 . i) in ( BoundedFunctions A) by Lm1;

                then

                consider qi be Function of A, REAL such that

                 A343: qi = (q2 . i) & (qi | A) is bounded;

                take x = (qi . t);

                thus thesis by A343;

              end;

              consider z be FinSequence of REAL such that

               A344: ( dom z) = ( Seg ( len (T . n))) & for i be Nat st i in ( Seg ( len (T . n))) holds R2[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 be 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 (D,i))), ( upper_bound ( divset (D,i))).] by A333, INTEGRA1: 4;

              

               A354: 1 <= i & i <= ( len D) by A350, FINSEQ_1: 1;

              then 1 <= i & (i + 0 ) <= (( len D) + 1) by XREAL_1: 7;

              then

               A355: i in ( Seg (( len D) + 1));

              (1 + 0 ) <= (i + 1) & i <= ( len D) by A350, FINSEQ_1: 1, XREAL_1: 7;

              then (1 + 0 ) <= (i + 1) <= (( len D) + 1) by XREAL_1: 7;

              then

               A356: (i + 1) in ( Seg (( len D) + 1));

              

               A357: (z . i) = r

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

                

                 B20: ( dom f0) = [.a, b.] & ( dom g1) = [.a, (D . i).] & ( dom g2) = ].(D . i), b.] & ( dom h1) = [.a, (D . (i - 1)).] & ( dom h2) = ].(D . (i - 1)), b.] by FUNCOP_1: 13;

                per cases ;

                  suppose

                   A358: i = 1;

                  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: (D . i) in [.a, b.] by A7, A332, INTEGRA1: 6;

                  

                   A362: ( lower_bound ( divset (D,i))) = ( lower_bound A) & ( upper_bound ( divset (D,i))) = (D . i) by A332, A358, INTEGRA1:def 4;

                  

                   A364: a < (D . i) by A264, A358;

                  

                   A365: ( Dp1 (m,D,(i + 1))) = (m . (D . ((i + 1) - 1))) by A356, defDp1, A358

                  .= (( [.a, (D . i).] --> 1) +* ( ].(D . i), b.] --> 0 )) by A8, A361, A364;

                  

                   A366: ( Dp1 (m,D,i)) = (m . ( lower_bound A)) by A355, A358, defDp1

                  .= ( [.a, b.] --> 0 ) by A8, A359, A360;

                  

                   A368: ( dom f0) = A by A7, FUNCOP_1: 13;

                  

                   A369: a <= (D . i) & (D . i) <= b by A361, XXREAL_1: 1;

                  

                   A370: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

                  .= A by A7, B20, A369, XXREAL_1: 167;

                  ( rng f0) c= REAL ;

                  then

                  reconsider f0 as Function of A, REAL by A368, FUNCT_2: 2;

                  ( rng f1) c= REAL ;

                  then

                  reconsider f1 as Function of A, REAL by A370, FUNCT_2: 2;

                  

                   A372: (qi . t) = (r * ((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;

                    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 thesis;

                  end;

                  

                   A373: t in [.a, (D . i).] by A359, A362, INTEGRA1: 4, A333;

                  

                  then

                   A375: (f1 . t) = (( [.a, (D . 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 thesis by A351, A372, A375;

                end;

                  suppose

                   A376: i <> 1;

                  then

                   A378: (D . (i - 1)) in [.a, b.] by A7, A332, INTEGRA1: 7;

                  

                   A377: (D . i) in [.a, b.] by A7, A332, INTEGRA1: 6;

                  

                   A379: ( lower_bound ( divset (D,i))) = (D . (i - 1)) & ( upper_bound ( divset (D,i))) = (D . i) by A332, A376, INTEGRA1:def 4;

                  (i - 1) in ( dom D) by A332, A376, INTEGRA1: 7;

                  then

                   A382: (D . (i - 1)) < (D . i) by A332, XREAL_1: 146, VALUED_0:def 13;

                  (D . (i - 1)) = a or (D . (i - 1)) in ].a, b.] by A376, A7, A332, INTEGRA1: 7, XXREAL_1: 6;

                  per cases by XXREAL_1: 2;

                    suppose

                     A384: a = (D . (i - 1));

                    (1 + 0 ) < (i + 1) by XREAL_1: 8, A354;

                    

                    then

                     A386: ( Dp1 (m,D,(i + 1))) = (m . (D . ((i + 1) - 1))) by A356, defDp1

                    .= (( [.a, (D . i).] --> 1) +* ( ].(D . i), b.] --> 0 )) by A8, A377, A384, A382;

                    

                     A387: ( Dp1 (m,D,i)) = (m . (D . (i - 1))) by A355, A376, defDp1

                    .= ( [.a, b.] --> 0 ) by A8, A378, A384;

                    

                     A389: ( dom f0) = A by A7, FUNCOP_1: 13;

                    

                     A390: a <= (D . i) & (D . i) <= b by A377, XXREAL_1: 1;

                    

                     A392: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

                    .= A by A7, B20, A390, XXREAL_1: 167;

                    ( rng f0) c= REAL ;

                    then

                    reconsider f0 as Function of A, REAL by A389, FUNCT_2: 2;

                    ( rng f1) c= REAL ;

                    then

                    reconsider f1 as Function of A, REAL by A392, FUNCT_2: 2;

                    

                     A394: (qi . t) = (r * ((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;

                      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 thesis;

                    end;

                    

                     A395: t in [.(D . (i - 1)), (D . i).] by A379, INTEGRA1: 4, A333;

                    a <= (D . (i - 1)) & (D . (i - 1)) <= b by A378, XXREAL_1: 1;

                    then

                     B396: [.(D . (i - 1)), (D . i).] c= [.a, (D . i).] by XXREAL_1: 34;

                    

                    then

                     A398: (f1 . t) = (( [.a, (D . 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 thesis by A351, A394, A398;

                  end;

                    suppose

                     A399: a < (D . (i - 1));

                    (1 + 0 ) < (i + 1) by XREAL_1: 8, A354;

                    

                    then

                     A401: ( Dp1 (m,D,(i + 1))) = (m . (D . ((i + 1) - 1))) by A356, defDp1

                    .= (( [.a, (D . i).] --> 1) +* ( ].(D . i), b.] --> 0 )) by A8, A377, A399, A382;

                    

                     A402: ( Dp1 (m,D,i)) = (m . (D . (i - 1))) by A355, A376, defDp1

                    .= (( [.a, (D . (i - 1)).] --> 1) +* ( ].(D . (i - 1)), b.] --> 0 )) by A8, A378, A399;

                    

                     A404: a <= (D . i) & (D . i) <= b by A377, XXREAL_1: 1;

                    

                     A405: a <= (D . (i - 1)) & (D . (i - 1)) <= b by A378, XXREAL_1: 1;

                    

                     A406: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

                    .= A by A7, B20, A404, XXREAL_1: 167;

                    

                     A407: ( dom f2) = (( dom h1) \/ ( dom h2)) by FUNCT_4:def 1

                    .= A by A7, B20, A405, XXREAL_1: 167;

                    ( rng f1) c= REAL ;

                    then

                    reconsider f1 as Function of A, REAL by A406, FUNCT_2: 2;

                    ( rng f2) c= REAL ;

                    then

                    reconsider f2 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,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;

                      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 thesis;

                    end;

                    

                     A410: t in [.(D . (i - 1)), (D . i).] by A379, INTEGRA1: 4, A333;

                    

                     B411: [.(D . (i - 1)), (D . i).] c= [.a, (D . i).] by A405, XXREAL_1: 34;

                    

                    then

                     A413: (f1 . t) = (( [.a, (D . i).] --> 1) . t) by A410, FUNCT_4: 16, B20, XXREAL_1: 90

                    .= 1 by B411, A410, FUNCOP_1: 7;

                    (D . (i - 1)) < t & t <= (D . i) by A332, INTEGRA1:def 4, A334, A376;

                    then

                     A414: t in ].(D . (i - 1)), b.] by A408;

                    

                    then (f2 . t) = (( ].(D . (i - 1)), b.] --> 0 ) . t) by B20, FUNCT_4: 13

                    .= 0 by A414, FUNCOP_1: 7;

                    hence thesis by A351, A409, A413;

                  end;

                end;

              end;

              for k be Nat st k in ( dom z) & k <> i holds (z . k) = 0

              proof

                let k be Nat;

                assume that

                 A415: k in ( dom z) and

                 A416: k <> i;

                consider r be 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 be Function of A, REAL such that

                 A423: qk = (q2 . k) & (z . k) = (qk . t) by A344, A415;

                

                 A425: k in ( dom D) by A344, A415, FINSEQ_1:def 3;

                

                 A426: 1 <= k <= ( len D) by A344, A415, FINSEQ_1: 1;

                then (k + 0 ) <= (( len D) + 1) by XREAL_1: 7;

                then

                 A427: k in ( Seg (( len D) + 1)) by A426;

                

                 e: (1 + 0 ) <= (k + 1) by XREAL_1: 7;

                (k + 1) <= (( len D) + 1) by XREAL_1: 7, A426;

                then

                 A428: (k + 1) in ( Seg (( len D) + 1)) by e;

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

                

                 B30: ( dom f0) = [.a, b.] & ( dom g1) = [.a, (D . k).] & ( dom g2) = ].(D . k), b.] & ( dom h1) = [.a, (D . (k - 1)).] & ( dom h2) = ].(D . (k - 1)), b.] by FUNCOP_1: 13;

                per cases ;

                  suppose

                   A429: k = 1;

                  then

                   A433: ( lower_bound ( divset (D,i))) = (D . (i - 1)) & ( upper_bound ( divset (D,i))) = (D . i) by A332, INTEGRA1:def 4, A416;

                  

                   A435: (i - 1) in ( dom D) by A332, A429, A416, INTEGRA1: 7;

                  

                   A440: (D . k) in [.a, b.] by A7, A425, INTEGRA1: 6;

                  then

                   A446: a <= (D . k) & (D . k) <= b by XXREAL_1: 1;

                  

                   A445: ( dom f0) = A by A7, FUNCOP_1: 13;

                  

                   A447: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

                  .= A by A7, B30, A446, XXREAL_1: 167;

                  ( rng f0) c= REAL ;

                  then

                  reconsider f0 as Function of A, REAL by A445, FUNCT_2: 2;

                  ( rng f1) c= REAL ;

                  then

                  reconsider f1 as Function of A, REAL by A447, FUNCT_2: 2;

                  

                   A451: a < (D . k) by A264, A429;

                  

                   A452: ( Dp1 (m,D,(k + 1))) = (m . (D . ((k + 1) - 1))) by A428, defDp1, A429

                  .= (( [.a, (D . k).] --> 1) +* ( ].(D . 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,D,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,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;

                    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 thesis;

                  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;

                  (D . k) <= (D . (i - 1))

                  proof

                    k = (i - 1) or k < (i - 1) by A456, XXREAL_0: 1;

                    hence thesis by A425, A435, VALUED_0:def 13;

                  end;

                  then

                   A457: (D . k) < t by A334, A429, A416, XXREAL_0: 2, A433;

                  a <= t <= b by XXREAL_1: 1, A7;

                  then

                   A459: t in ].(D . k), b.] by A457;

                  

                  then

                   A461: (f1 . t) = (( ].(D . k), b.] --> 0 ) . t) by B30, FUNCT_4: 13

                  .= 0 by A459, FUNCOP_1: 7;

                  (f0 . t) = 0 by A7, FUNCOP_1: 7;

                  hence thesis by A423, A453, A461;

                end;

                  suppose

                   A462: k <> 1;

                  then

                   A464: (D . (k - 1)) in [.a, b.] by A7, A425, INTEGRA1: 7;

                  

                   A463: (D . k) in [.a, b.] by A7, A425, INTEGRA1: 6;

                  

                   A467: (k - 1) in ( dom D) by A425, A462, INTEGRA1: 7;

                  then

                   A468: (D . (k - 1)) < (D . 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 D) by A426, XXREAL_0: 2;

                  then

                   A471: 1 in ( dom D) by FINSEQ_3: 25;

                  (D . 1) <= (D . (k - 1))

                  proof

                    1 = (k - 1) or 1 < (k - 1) by A470, XXREAL_0: 1;

                    hence thesis by A467, A471, VALUED_0:def 13;

                  end;

                  then

                   A472: a < (D . (k - 1)) by A264, XXREAL_0: 2;

                  (1 + 0 ) < (k + 1) by XREAL_1: 8, A426;

                  

                  then

                   A474: ( Dp1 (m,D,(k + 1))) = (m . (D . ((k + 1) - 1))) by A428, defDp1

                  .= (( [.a, (D . k).] --> 1) +* ( ].(D . k), b.] --> 0 )) by A8, A463, A472, A468;

                  

                   A475: ( Dp1 (m,D,k)) = (m . (D . (k - 1))) by A427, A462, defDp1

                  .= (( [.a, (D . (k - 1)).] --> 1) +* ( ].(D . (k - 1)), b.] --> 0 )) by A8, A464, A472;

                  

                   A477: a <= (D . k) & (D . k) <= b by A463, XXREAL_1: 1;

                  

                   A478: a <= (D . (k - 1)) & (D . (k - 1)) <= b by A464, XXREAL_1: 1;

                  

                   A479: ( dom f1) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

                  .= A by A7, B30, A477, XXREAL_1: 167;

                  

                   A480: ( dom f2) = (( dom h1) \/ ( dom h2)) by FUNCT_4:def 1

                  .= A by A7, B30, A478, XXREAL_1: 167;

                  ( rng f1) c= REAL ;

                  then

                  reconsider f1 as Function of A, REAL by A479, FUNCT_2: 2;

                  ( rng f2) c= REAL ;

                  then

                  reconsider f2 as Function of A, REAL by A480, FUNCT_2: 2;

                  

                   A482: (qk . t) = (r * ((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;

                    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 thesis;

                  end;

                  per cases by A416, XXREAL_0: 1;

                    suppose i < k;

                    then (i + 1) <= k by NAT_1: 13;

                    then

                     A485: ((i + 1) - 1) <= (k - 1) by XREAL_1: 13;

                    

                     A486: (D . i) <= (D . (k - 1))

                    proof

                      i = (k - 1) or i < (k - 1) by A485, XXREAL_0: 1;

                      hence thesis by A332, A467, VALUED_0:def 13;

                    end;

                    

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

                    proof

                      per cases ;

                        suppose i = 1;

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

                      end;

                        suppose i <> 1;

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

                      end;

                    end;

                    a <= t & t <= ( upper_bound ( divset (D,i))) by B352, XXREAL_1: 1, A7;

                    then

                     A489: a <= t & t <= (D . (k - 1)) by A488, XXREAL_0: 2;

                    then

                     A490: t in [.a, (D . (k - 1)).];

                    a <= t & t <= (D . k) by A468, A489, XXREAL_0: 2;

                    then

                     A491: t in [.a, (D . k).];

                    

                    then

                     A494: (f1 . t) = (( [.a, (D . k).] --> 1) . t) by FUNCT_4: 16, B30, XXREAL_1: 90

                    .= 1 by A491, FUNCOP_1: 7;

                    (f2 . t) = (( [.a, (D . (k - 1)).] --> 1) . t) by A490, FUNCT_4: 16, B30, XXREAL_1: 90

                    .= 1 by A490, FUNCOP_1: 7;

                    hence thesis by A423, A482, A494;

                  end;

                    suppose

                     A496: k < i;

                    then (k + 1) <= i by NAT_1: 13;

                    then

                     A499: ((k + 1) - 1) <= (i - 1) by XREAL_1: 13;

                    

                     A500: (i - 1) in ( dom D) by A332, A496, A426, INTEGRA1: 7;

                    

                     A502: (D . k) <= (D . (i - 1))

                    proof

                      k = (i - 1) or k < (i - 1) by A499, XXREAL_0: 1;

                      hence thesis by A425, A500, VALUED_0:def 13;

                    end;

                    (D . (i - 1)) < t by A496, A426, A334, A332, INTEGRA1:def 4;

                    then

                     A504: (D . k) < t by A502, XXREAL_0: 2;

                    then

                     A505: (D . (k - 1)) < t by A468, XXREAL_0: 2;

                    

                     A506: a <= t & t <= b by XXREAL_1: 1, A7;

                    then

                     A507: t in ].(D . k), b.] by A504;

                    

                    then

                     A509: (f1 . t) = (( ].(D . k), b.] --> 0 ) . t) by B30, FUNCT_4: 13

                    .= 0 by A507, FUNCOP_1: 7;

                    

                     A508: t in ].(D . (k - 1)), b.] by A505, A506;

                    

                    then (f2 . t) = (( ].(D . (k - 1)), b.] --> 0 ) . t) by B30, FUNCT_4: 13

                    .= 0 by A508, FUNCOP_1: 7;

                    hence thesis by A423, A482, A509;

                  end;

                end;

              end;

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

            end;

            

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

            proof

              let t be Element of A;

              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 be 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 be 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;

                assume

                 A544: tD in ( dom g) & t in ( dom g) & |.(tD - t).| < s;

                

                 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;

              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: |.(tD - t).| < s by A329, A540, A541, INTEGR20: 12;

              (g1 . t) = (g . tD) by A331, A540, A541, A542;

              hence |.((g1 . t) - (g . t)).| < (r / 2) by B551, A543, A549, A260, A317;

            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 be Function of A, REAL such that

             A552: g2 = g0 & (g2 | A) is bounded;

            now

              let k be Real;

              assume k in ( PreNorms g0);

              then

              consider t be 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;

            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 thesis by A321, XXREAL_0: 2;

          end;

          take m0;

          thus thesis by A325;

        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 V by FUNCT_2:def 1;

        then

         A557: ( rng xD) c= ( dom f);

        v in the carrier of V;

        then

         A558: v in ( dom f) by FUNCT_2:def 1;

        consider K be Real such that

         A559: 0 <= K & for x be Point of V holds |.(f . x).| <= (K * ||.x.||) by DUALSP01:def 9;

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Point of V st x1 in ( dom f) & ||.(x1 - v).|| < s holds |.((f /. x1) - (f /. v)).| < r

        proof

          let r be Real;

          assume

           A561: 0 < r;

          reconsider s = (r / (K + 1)) as Real;

          

           A563: for x1 be Point of V st x1 in ( dom f) & ||.(x1 - v).|| < s holds |.((f /. x1) - (f /. v)).| < r

          proof

            let x1 be Point of V;

            assume that x1 in ( dom f) and

             A565: ||.(x1 - v).|| < s;

             |.((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;

          end;

          take s;

          thus thesis by A559, A561, XREAL_1: 139, A563;

        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;

      end;

      then

       B573: ||.x.|| <= ( total_vd rho) by A251, Lm83;

      take rho;

      thus thesis by B250, A259, B573, A258, XXREAL_0: 1;

    end;