c0sp2.miz

    begin

    definition

      let X be 1-sorted, y be Real;

      :: C0SP2:def1

      func X --> y -> RealMap of X equals (the carrier of X --> y);

      coherence

      proof

        y in REAL by XREAL_0:def 1;

        hence thesis by FUNCOP_1: 45;

      end;

    end

    registration

      let X be TopSpace, y be Real;

      cluster (X --> y) -> continuous;

      coherence

      proof

        set f = (X --> y);

        set HX = ( [#] X);

        let P1 be Subset of REAL such that P1 is closed;

        per cases ;

          suppose y in P1;

          then (f " P1) = HX by FUNCOP_1: 14;

          hence (f " P1) is closed;

        end;

          suppose not y in P1;

          then (f " P1) = ( {} X) by FUNCOP_1: 16;

          hence (f " P1) is closed;

        end;

      end;

    end

    theorem :: C0SP2:1



     Th1: for X be non empty TopSpace, f be RealMap of X holds f is continuous iff for x be Point of X, 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 non empty TopSpace, f be RealMap of X;

      hereby

        assume

         A1: f is continuous;

        now

          let x be Point of X, V be Subset of REAL ;

          set r = (f . x);

          assume r in V & V is open;

          then

          consider r0 be Real such that

           A2: 0 < r0 & ].(r - r0), (r + r0).[ c= V by RCOMP_1: 19;

          set S = ].(r - r0), (r + r0).[;

          take W = (f " S);

           |.(r - r).| < r0 by A2, COMPLEX1: 44;

          then r in S by RCOMP_1: 1;

          hence x in W by FUNCT_2: 38;

          thus W is open by A1, PSCOMP_1: 8;

          (f .: (f " S)) c= S by FUNCT_1: 75;

          hence (f .: W) c= V by A2;

        end;

        hence for x be Point of X, 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;

      end;

      assume

       A3: for x be Point of X, 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;

      now

        let Y be Subset of REAL ;

        assume Y is closed;

        then ((Y ` ) ` ) is closed;

        then

         A4: (Y ` ) is open;

        for x be Point of X st x in ((f " Y) ` ) holds ex W be Subset of X st W is a_neighborhood of x & W c= ((f " Y) ` )

        proof

          let x be Point of X;

          assume x in ((f " Y) ` );

          then x in (f " (Y ` )) by FUNCT_2: 100;

          then (f . x) in (Y ` ) by FUNCT_2: 38;

          then

          consider V be Subset of REAL such that

           A5: (f . x) in V & V is open & V c= (Y ` ) by A4;

          consider W be Subset of X such that

           A6: x in W & W is open & (f .: W) c= V by A3, A5;

          take W;

          thus W is a_neighborhood of x by A6, CONNSP_2: 3;

          (f .: W) c= (Y ` ) by A5, A6;

          then

           A7: (f " (f .: W)) c= (f " (Y ` )) by RELAT_1: 143;

          W c= (f " (f .: W)) by FUNCT_2: 42;

          then W c= (f " (Y ` )) by A7;

          hence W c= ((f " Y) ` ) by FUNCT_2: 100;

        end;

        then ((f " Y) ` ) is open by CONNSP_2: 7;

        then (((f " Y) ` ) ` ) is closed by TOPS_1: 4;

        hence (f " Y) is closed;

      end;

      hence f is continuous;

    end;

    definition

      let X be non empty TopSpace;

      :: C0SP2:def2

      func ContinuousFunctions (X) -> Subset of ( RAlgebra the carrier of X) equals the set of all f where f be continuous RealMap of X;

      correctness

      proof

        set A = the set of all f where f be continuous RealMap of X;

        A c= ( Funcs (the carrier of X, REAL ))

        proof

          let x be object;

          assume x in A;

          then ex f be continuous RealMap of X st x = f;

          hence x in ( Funcs (the carrier of X, REAL )) by FUNCT_2: 8;

        end;

        hence thesis;

      end;

    end

    registration

      let X be non empty TopSpace;

      cluster ( ContinuousFunctions X) -> non empty;

      coherence

      proof

        (X --> 0 ) in the set of all f where f be continuous RealMap of X;

        hence thesis;

      end;

    end

    registration

      let X be non empty TopSpace;

      cluster ( ContinuousFunctions X) -> additively-linearly-closed multiplicatively-closed;

      coherence

      proof

        set W = ( ContinuousFunctions X);

        set V = ( RAlgebra the carrier of X);



         A1: ( RAlgebra the carrier of X) is RealLinearSpace by C0SP1: 7;

        for v,u be Element of V st v in W & u in W holds (v + u) in W

        proof

          let v,u be Element of V such that

           A2: v in W & u in W;

          consider v1 be continuous RealMap of X such that

           A3: v1 = v by A2;

          consider u1 be continuous RealMap of X such that

           A4: u1 = u by A2;



           A5: (v1 + u1) is Function of the carrier of X, REAL & (v1 + u1) is continuous by NAGATA_1: 22;

          reconsider h = (v + u) as Element of ( Funcs (the carrier of X, REAL ));



           A6: ex f be Function st h = f & ( dom f) = the carrier of X & ( rng f) c= REAL by FUNCT_2:def 2;

          (( dom v1) /\ ( dom u1)) = (the carrier of X /\ ( dom u1)) by FUNCT_2:def 1;

          then

           A7: (( dom v1) /\ ( dom u1)) = (the carrier of X /\ the carrier of X) by FUNCT_2:def 1;

          for x be object st x in ( dom h) holds (h . x) = ((v1 . x) + (u1 . x)) by A3, A4, FUNCSDOM: 1;

          then (v + u) = (v1 + u1) by A7, A6, VALUED_1:def 1;

          hence (v + u) in W by A5;

        end;

        then

         A8: W is add-closed by IDEAL_1:def 1;

        for v be Element of V st v in W holds ( - v) in W

        proof

          let v be Element of V such that

           A9: v in W;

          consider v1 be continuous RealMap of X such that

           A10: v1 = v by A9;



           A11: ( - v1) is continuous RealMap of X by PSCOMP_1: 9;

          reconsider h = ( - v), v2 = v as Element of ( Funcs (the carrier of X, REAL ));



           A12: h = (( - 1) * v) by A1, RLVECT_1: 16;



           A13: ex f be Function st h = f & ( dom f) = the carrier of X & ( rng f) c= REAL by FUNCT_2:def 2;



           A14: ( dom v1) = the carrier of X by FUNCT_2:def 1;

          now

            let x be object;

            assume x in ( dom h);

            then

            reconsider y = x as Element of the carrier of X;

            (h . x) = (( - 1) * (v2 . y)) by A12, FUNCSDOM: 4;

            hence (h . x) = ( - (v1 . x)) by A10;

          end;

          then ( - v) = ( - v1) by A14, A13, VALUED_1: 9;

          hence ( - v) in W by A11;

        end;

        then

         A15: W is having-inverse;

        for a be Real, u be Element of V st u in W holds (a * u) in W

        proof

          let a be Real, u be Element of V such that

           A16: u in W;

          consider u1 be continuous RealMap of X such that

           A17: u1 = u by A16;



           A18: (a (#) u1) is continuous RealMap of X

          proof

            reconsider U = u1 as continuous Function of X, R^1 by JORDAN5A: 27, TOPMETR: 17;

            set c = the carrier of X;

            consider H be Function of X, R^1 such that

             A19: for p be Point of X holds for r1 be Real st (U . p) = r1 holds (H . p) = (a * r1) and

             A20: H is continuous by JGRAPH_2: 23;

            reconsider h = H as RealMap of X by TOPMETR: 17;



             A21: ( dom h) = the carrier of X by FUNCT_2:def 1

            .= ( dom u1) by FUNCT_2:def 1;

            for c be object st c in ( dom h) holds (h . c) = (a * (u1 . c)) by A19;

            then h = (a (#) u1) by A21, VALUED_1:def 5;

            hence (a (#) u1) is continuous RealMap of X by A20, JORDAN5A: 27;

          end;

          reconsider h = (a * u) as Element of ( Funcs (the carrier of X, REAL ));



           A22: ex f be Function st h = f & ( dom f) = the carrier of X & ( rng f) c= REAL by FUNCT_2:def 2;



           A23: ( dom u1) = the carrier of X by FUNCT_2:def 1;

          for x be object st x in ( dom h) holds (h . x) = (a * (u1 . x)) by A17, FUNCSDOM: 4;

          then (a * u) = (a (#) u1) by A23, A22, VALUED_1:def 5;

          hence (a * u) in W by A18;

        end;

        hence ( ContinuousFunctions X) is additively-linearly-closed by A8, A15;



         A24: for v,u be Element of V st v in W & u in W holds (v * u) in W

        proof

          let v,u be Element of V such that

           A25: v in W & u in W;

          consider v1 be continuous RealMap of X such that

           A26: v1 = v by A25;

          consider u1 be continuous RealMap of X such that

           A27: u1 = u by A25;



           A28: (v1 (#) u1) is continuous RealMap of X

          proof

            reconsider V = v1, U = u1 as continuous Function of X, R^1 by JORDAN5A: 27, TOPMETR: 17;

            consider H be Function of X, R^1 such that

             A29: for p be Point of X holds for r1,r2 be Real st (V . p) = r1 & (U . p) = r2 holds (H . p) = (r1 * r2) and

             A30: H is continuous by JGRAPH_2: 25;

            reconsider h = H as RealMap of X by TOPMETR: 17;



             A31: ( dom h) = (the carrier of X /\ the carrier of X) by FUNCT_2:def 1

            .= (the carrier of X /\ ( dom u1)) by FUNCT_2:def 1

            .= (( dom v1) /\ ( dom u1)) by FUNCT_2:def 1;

            for c be object st c in ( dom h) holds (h . c) = ((v1 . c) * (u1 . c)) by A29;

            then h = (v1 (#) u1) by A31, VALUED_1:def 4;

            hence (v1 (#) u1) is continuous RealMap of X by A30, JORDAN5A: 27;

          end;

          reconsider h = (v * u) as Element of ( Funcs (the carrier of X, REAL ));



           A32: ex f be Function st h = f & ( dom f) = the carrier of X & ( rng f) c= REAL by FUNCT_2:def 2;

          (( dom v1) /\ ( dom u1)) = (the carrier of X /\ ( dom u1)) by FUNCT_2:def 1;

          then

           A33: (( dom v1) /\ ( dom u1)) = (the carrier of X /\ the carrier of X) by FUNCT_2:def 1;

          for x be object st x in ( dom h) holds (h . x) = ((v1 . x) * (u1 . x)) by A26, A27, FUNCSDOM: 2;

          then (v * u) = (v1 (#) u1) by A33, A32, VALUED_1:def 4;

          hence (v * u) in W by A28;

        end;

        reconsider g = ( RealFuncUnit the carrier of X) as RealMap of X;

        g = (X --> 1);

        then ( 1. V) in W;

        hence thesis by A24;

      end;

    end

    definition

      let X be non empty TopSpace;

      :: C0SP2:def3

      func R_Algebra_of_ContinuousFunctions (X) -> AlgebraStr equals AlgebraStr (# ( ContinuousFunctions X), ( mult_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( Add_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( Mult_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( One_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( Zero_ (( ContinuousFunctions X),( RAlgebra the carrier of X))) #);

      coherence ;

    end

    theorem :: C0SP2:2

    for X be non empty TopSpace holds ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

    registration

      let X be non empty TopSpace;

      cluster ( R_Algebra_of_ContinuousFunctions X) -> strict non empty;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      cluster ( R_Algebra_of_ContinuousFunctions X) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative;

      coherence

      proof

        now

          let v be VECTOR of ( R_Algebra_of_ContinuousFunctions X);

          reconsider v1 = v as VECTOR of ( RAlgebra the carrier of X) by TARSKI:def 3;

          ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

          then (1 * v) = (1 * v1) by C0SP1: 8;

          hence (1 * v) = v by FUNCSDOM: 12;

        end;

        hence thesis by C0SP1: 6;

      end;

    end

    theorem :: C0SP2:3



     Th3: for X be non empty TopSpace holds for F,G,H be VECTOR of ( R_Algebra_of_ContinuousFunctions X) holds for f,g,h be RealMap of X holds (f = F & g = G & h = H implies (H = (F + G) iff (for x be Element of the carrier of X holds (h . x) = ((f . x) + (g . x)))))

    proof

      let X be non empty TopSpace;

      let F,G,H be VECTOR of ( R_Algebra_of_ContinuousFunctions X);

      let f,g,h be RealMap of X;

      assume

       A1: f = F & g = G & h = H;



       A2: ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

      reconsider f1 = F, g1 = G, h1 = H as VECTOR of ( RAlgebra the carrier of X) by TARSKI:def 3;

      hereby

        assume

         A3: H = (F + G);

        let x be Element of the carrier of X;

        h1 = (f1 + g1) by A2, A3, C0SP1: 8;

        hence (h . x) = ((f . x) + (g . x)) by A1, FUNCSDOM: 1;

      end;

      assume for x be Element of X holds (h . x) = ((f . x) + (g . x));

      then h1 = (f1 + g1) by A1, FUNCSDOM: 1;

      hence H = (F + G) by A2, C0SP1: 8;

    end;

    theorem :: C0SP2:4



     Th4: for X be non empty TopSpace holds for F,G,H be VECTOR of ( R_Algebra_of_ContinuousFunctions X) holds for f,g,h be RealMap of X holds for a be Real holds (f = F & g = G implies (G = (a * F) iff for x be Element of X holds (g . x) = (a * (f . x))))

    proof

      let X be non empty TopSpace;

      let F,G,H be VECTOR of ( R_Algebra_of_ContinuousFunctions X);

      let f,g,h be RealMap of X;

      let a be Real;

      assume

       A1: f = F & g = G;



       A2: ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

      reconsider f1 = F, g1 = G as VECTOR of ( RAlgebra the carrier of X) by TARSKI:def 3;

      hereby

        assume

         A3: G = (a * F);

        let x be Element of the carrier of X;

        g1 = (a * f1) by A2, A3, C0SP1: 8;

        hence (g . x) = (a * (f . x)) by A1, FUNCSDOM: 4;

      end;

      assume for x be Element of the carrier of X holds (g . x) = (a * (f . x));

      then g1 = (a * f1) by A1, FUNCSDOM: 4;

      hence G = (a * F) by A2, C0SP1: 8;

    end;

    theorem :: C0SP2:5



     Th5: for X be non empty TopSpace holds for F,G,H be VECTOR of ( R_Algebra_of_ContinuousFunctions X) holds for f,g,h be RealMap of X holds (f = F & g = G & h = H implies (H = (F * G) iff (for x be Element of the carrier of X holds (h . x) = ((f . x) * (g . x)))))

    proof

      let X be non empty TopSpace;

      let F,G,H be VECTOR of ( R_Algebra_of_ContinuousFunctions X);

      let f,g,h be RealMap of X;

      assume

       A1: f = F & g = G & h = H;



       A2: ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

      reconsider f1 = F, g1 = G, h1 = H as VECTOR of ( RAlgebra the carrier of X) by TARSKI:def 3;

      hereby

        assume

         A3: H = (F * G);

        let x be Element of the carrier of X;

        h1 = (f1 * g1) by A2, A3, C0SP1: 8;

        hence (h . x) = ((f . x) * (g . x)) by A1, FUNCSDOM: 2;

      end;

      assume for x be Element of X holds (h . x) = ((f . x) * (g . x));

      then h1 = (f1 * g1) by A1, FUNCSDOM: 2;

      hence H = (F * G) by A2, C0SP1: 8;

    end;

    theorem :: C0SP2:6



     Th6: for X be non empty TopSpace holds ( 0. ( R_Algebra_of_ContinuousFunctions X)) = (X --> 0 )

    proof

      let X be non empty TopSpace;



       A1: ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

      ( 0. ( RAlgebra the carrier of X)) = (X --> 0 );

      hence thesis by A1, C0SP1: 8;

    end;

    theorem :: C0SP2:7



     Th7: for X be non empty TopSpace holds ( 1_ ( R_Algebra_of_ContinuousFunctions X)) = (X --> 1)

    proof

      let X be non empty TopSpace;



       A1: ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

      ( 1_ ( RAlgebra the carrier of X)) = (X --> 1);

      hence thesis by A1, C0SP1: 8;

    end;

    theorem :: C0SP2:8



     Th8: for A be Algebra, A1,A2 be Subalgebra of A holds the carrier of A1 c= the carrier of A2 implies A1 is Subalgebra of A2

    proof

      let A be Algebra, A1,A2 be Subalgebra of A;

      assume

       A1: the carrier of A1 c= the carrier of A2;

      set CA1 = the carrier of A1;

      set CA2 = the carrier of A2;

      set AA = the addF of A;

      set mA = the multF of A;

      set MA = the Mult of A;



       A2: ( 0. A1) = ( 0. A) & ( 0. A2) = ( 0. A) & ( 1. A1) = ( 1. A) & ( 1. A2) = ( 1. A) by C0SP1:def 9;



       A3: the addF of A1 = (the addF of A2 || the carrier of A1)

      proof

        the addF of A1 = (AA || CA1) & the addF of A2 = (AA || CA2) & [:CA1, CA1:] c= [:CA2, CA2:] by A1, C0SP1:def 9, ZFMISC_1: 96;

        hence thesis by FUNCT_1: 51;

      end;



       A4: the multF of A1 = (the multF of A2 || the carrier of A1)

      proof

        the multF of A1 = (mA || CA1) & the multF of A2 = (mA || CA2) & [:CA1, CA1:] c= [:CA2, CA2:] by A1, C0SP1:def 9, ZFMISC_1: 96;

        hence thesis by FUNCT_1: 51;

      end;

      the Mult of A1 = (the Mult of A2 | [: REAL , CA1:])

      proof

        the Mult of A1 = (MA | [: REAL , CA1:]) & the Mult of A2 = (MA | [: REAL , CA2:]) & [: REAL , CA1:] c= [: REAL , CA2:] by A1, C0SP1:def 9, ZFMISC_1: 96;

        hence thesis by FUNCT_1: 51;

      end;

      hence thesis by A1, A2, A3, A4, C0SP1:def 9;

    end;



     Lm1: for X be compact non empty TopSpace holds for x be set st x in ( ContinuousFunctions X) holds x in ( BoundedFunctions the carrier of X)

    proof

      let X be compact non empty TopSpace;

      let x be set;

      assume x in ( ContinuousFunctions X);

      then

      consider h be continuous RealMap of X such that

       A1: x = h;



       A2: h is bounded_above & h is bounded_below by SEQ_2:def 8;

      then

      consider r1 be Real such that

       A3: for y be object st y in ( dom h) holds (h . y) < r1 by SEQ_2:def 1;



       A4: (the carrier of X /\ ( dom h)) c= ( dom h) by XBOOLE_1: 17;

      then for y be object st y in (the carrier of X /\ ( dom h)) holds (h . y) <= r1 by A3;

      then

       A5: (h | the carrier of X) is bounded_above by RFUNCT_1: 70;

      consider r2 be Real such that

       A6: for y be object st y in ( dom h) holds r2 < (h . y) by A2, SEQ_2:def 2;

      for y be object st y in (the carrier of X /\ ( dom h)) holds r2 <= (h . y) by A4, A6;

      then

       A7: (h | the carrier of X) is bounded_below by RFUNCT_1: 71;

      (the carrier of X /\ the carrier of X) = the carrier of X;

      then (h | the carrier of X) is bounded by A5, A7, RFUNCT_1: 75;

      hence x in ( BoundedFunctions the carrier of X) by A1;

    end;

    theorem :: C0SP2:9

    for X be compact non empty TopSpace holds (( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( R_Algebra_of_BoundedFunctions the carrier of X))

    proof

      let X be compact non empty TopSpace;



       A1: the carrier of ( R_Algebra_of_ContinuousFunctions X) c= the carrier of ( R_Algebra_of_BoundedFunctions the carrier of X) by Lm1;



       A2: ( R_Algebra_of_ContinuousFunctions X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 6;

      ( R_Algebra_of_BoundedFunctions the carrier of X) is Subalgebra of ( RAlgebra the carrier of X) by C0SP1: 10;

      hence thesis by A1, A2, Th8;

    end;

    definition

      let X be compact non empty TopSpace;

      :: C0SP2:def4

      func ContinuousFunctionsNorm (X) -> Function of ( ContinuousFunctions X), REAL equals (( BoundedFunctionsNorm the carrier of X) | ( ContinuousFunctions X));

      correctness

      proof

        for x be object st x in ( ContinuousFunctions X) holds x in ( BoundedFunctions the carrier of X) by Lm1;

        then ( ContinuousFunctions X) c= ( BoundedFunctions the carrier of X);

        hence thesis by FUNCT_2: 32;

      end;

    end

    definition

      let X be compact non empty TopSpace;

      :: C0SP2:def5

      func R_Normed_Algebra_of_ContinuousFunctions (X) -> Normed_AlgebraStr equals Normed_AlgebraStr (# ( ContinuousFunctions X), ( mult_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( Add_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( Mult_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( One_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( Zero_ (( ContinuousFunctions X),( RAlgebra the carrier of X))), ( ContinuousFunctionsNorm X) #);

      correctness ;

    end

    registration

      let X be compact non empty TopSpace;

      cluster ( R_Normed_Algebra_of_ContinuousFunctions X) -> strict non empty;

      correctness ;

    end

     Lm2:

    now

      let X be compact non empty TopSpace;

      set F = ( R_Normed_Algebra_of_ContinuousFunctions X);

      let x,e be Element of F;

      assume

       A1: e = ( One_ (( ContinuousFunctions X),( RAlgebra the carrier of X)));

      set X1 = ( ContinuousFunctions X);

      reconsider f = x as Element of X1;

      ( 1_ ( RAlgebra the carrier of X)) = (X --> 1)

      .= ( 1_ ( R_Algebra_of_ContinuousFunctions X)) by Th7;

      then

       A2: [f, ( 1_ ( RAlgebra the carrier of X))] in [:X1, X1:] & [( 1_ ( RAlgebra the carrier of X)), f] in [:X1, X1:] by ZFMISC_1: 87;

      (x * e) = (( mult_ (X1,( RAlgebra the carrier of X))) . (f,( 1_ ( RAlgebra the carrier of X)))) by A1, C0SP1:def 8;

      then (x * e) = ((the multF of ( RAlgebra the carrier of X) || X1) . (f,( 1_ ( RAlgebra the carrier of X)))) by C0SP1:def 6;

      then (x * e) = (f * ( 1_ ( RAlgebra the carrier of X))) by A2, FUNCT_1: 49;

      hence (x * e) = x;

      (e * x) = (( mult_ (X1,( RAlgebra the carrier of X))) . (( 1_ ( RAlgebra the carrier of X)),f)) by A1, C0SP1:def 8;

      then (e * x) = ((the multF of ( RAlgebra the carrier of X) || X1) . (( 1_ ( RAlgebra the carrier of X)),f)) by C0SP1:def 6;

      then (e * x) = (( 1_ ( RAlgebra the carrier of X)) * f) by A2, FUNCT_1: 49;

      hence (e * x) = x;

    end;

    registration

      let X be compact non empty TopSpace;

      cluster ( R_Normed_Algebra_of_ContinuousFunctions X) -> unital;

      correctness

      proof

        reconsider e = ( One_ (( ContinuousFunctions X),( RAlgebra the carrier of X))) as Element of ( R_Normed_Algebra_of_ContinuousFunctions X);

        take e;

        thus thesis by Lm2;

      end;

    end

    theorem :: C0SP2:10



     Th10: for W be Normed_AlgebraStr, V be Algebra st the AlgebraStr of W = V holds W is Algebra

    proof

      let W be Normed_AlgebraStr, V be Algebra such that

       A1: the AlgebraStr of W = V;

      reconsider W as non empty AlgebraStr by A1;



       A2: for x,y be VECTOR of W holds (x + y) = (y + x)

      proof

        let x,y be VECTOR of W;

        reconsider x1 = x, y1 = y as VECTOR of V by A1;

        (x + y) = (x1 + y1) by A1;

        then (x + y) = (y1 + x1);

        hence (x + y) = (y + x) by A1;

      end;



       A3: for x,y,z be VECTOR of W holds ((x + y) + z) = (x + (y + z))

      proof

        let x,y,z be VECTOR of W;

        reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1;

        ((x + y) + z) = ((x1 + y1) + z1) by A1;

        then ((x + y) + z) = (x1 + (y1 + z1)) by RLVECT_1:def 3;

        hence ((x + y) + z) = (x + (y + z)) by A1;

      end;



       A4: for x be VECTOR of W holds (x + ( 0. W)) = x

      proof

        let x be VECTOR of W;

        reconsider y = x as VECTOR of V by A1;

        (x + ( 0. W)) = (y + ( 0. V)) by A1;

        hence (x + ( 0. W)) = x by RLVECT_1: 4;

      end;



       A5: for x be Element of W holds x is right_complementable

      proof

        let x be Element of W;

        reconsider x1 = x as Element of V by A1;

        consider v be Element of V such that

         A6: (x1 + v) = ( 0. V) by ALGSTR_0:def 11;

        reconsider y = v as Element of W by A1;

        (x + y) = ( 0. W) by A6, A1;

        hence thesis;

      end;



       A7: for v,w be Element of W holds (v * w) = (w * v)

      proof

        let v,w be Element of W;

        reconsider v1 = v, w1 = w as Element of V by A1;

        (v * w) = (v1 * w1) by A1;

        then (v * w) = (w1 * v1);

        hence (v * w) = (w * v) by A1;

      end;



       A8: for a,b,x be Element of W holds ((a * b) * x) = (a * (b * x))

      proof

        let a,b,x be Element of W;

        reconsider y = x, a1 = a, b1 = b as Element of V by A1;

        ((a * b) * x) = ((a1 * b1) * y) by A1;

        then ((a * b) * x) = (a1 * (b1 * y)) by GROUP_1:def 3;

        hence ((a * b) * x) = (a * (b * x)) by A1;

      end;



       A9: W is right_unital

      proof

        let x be Element of W;

        reconsider x1 = x as Element of V by A1;

        (x * ( 1. W)) = (x1 * ( 1. V)) by A1;

        hence (x * ( 1. W)) = x;

      end;



       A10: W is right-distributive

      proof

        let x,y,z be Element of W;

        reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;

        (x * (y + z)) = (x1 * (y1 + z1)) by A1;

        then (x * (y + z)) = ((x1 * y1) + (x1 * z1)) by VECTSP_1:def 2;

        hence (x * (y + z)) = ((x * y) + (x * z)) by A1;

      end;

      W is vector-distributive scalar-distributive scalar-associative vector-associative

      proof

        thus W is vector-distributive

        proof

          let a be Real;

          let x,y be Element of W;

          reconsider x1 = x, y1 = y as Element of V by A1;

          (a * (x + y)) = (a * (x1 + y1)) by A1;

          then (a * (x + y)) = ((a * x1) + (a * y1)) by RLVECT_1:def 5;

          hence (a * (x + y)) = ((a * x) + (a * y)) by A1;

        end;

        thus W is scalar-distributive

        proof

          let a,b be Real;

          let x be Element of W;

          reconsider x1 = x as Element of V by A1;

          ((a + b) * x) = ((a + b) * x1) by A1;

          then ((a + b) * x) = ((a * x1) + (b * x1)) by RLVECT_1:def 6;

          hence ((a + b) * x) = ((a * x) + (b * x)) by A1;

        end;

        thus W is scalar-associative

        proof

          let a,b be Real;

          let x be Element of W;

          reconsider x1 = x as Element of V by A1;

          ((a * b) * x) = ((a * b) * x1) by A1;

          then ((a * b) * x) = (a * (b * x1)) by RLVECT_1:def 7;

          hence ((a * b) * x) = (a * (b * x)) by A1;

        end;

        let x,y be Element of W;

        let a be Real;

        reconsider x1 = x, y1 = y as Element of V by A1;

        (a * (x * y)) = (a * (x1 * y1)) by A1;

        then (a * (x * y)) = ((a * x1) * y1) by FUNCSDOM:def 9;

        hence (a * (x * y)) = ((a * x) * y) by A1;

      end;

      hence thesis by A2, A3, A4, A5, A7, A8, A9, A10, ALGSTR_0:def 16, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

    end;



     Lm3: for X be compact non empty TopSpace holds for x be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds ||.x.|| = ||.y.|| by FUNCT_1: 49;



     Lm4: for X be compact non empty TopSpace holds for x1,x2 be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds (x1 + x2) = (y1 + y2)

    proof

      let X be compact non empty TopSpace;

      let x1,x2 be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

      assume

       A1: x1 = y1 & x2 = y2;



      thus (x1 + x2) = ((the addF of ( RAlgebra the carrier of X) || ( ContinuousFunctions X)) . [x1, x2]) by C0SP1:def 5

      .= (the addF of ( RAlgebra the carrier of X) . [x1, x2]) by FUNCT_1: 49

      .= ((the addF of ( RAlgebra the carrier of X) || ( BoundedFunctions the carrier of X)) . [y1, y2]) by A1, FUNCT_1: 49

      .= (y1 + y2) by C0SP1:def 5;

    end;



     Lm5: for X be compact non empty TopSpace holds for a be Real, x be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds (a * x) = (a * y)

    proof

      let X be compact non empty TopSpace;

      let a be Real, x be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

      assume

       A1: x = y;

      reconsider aa = a as Element of REAL by XREAL_0:def 1;



      thus (a * x) = ((the Mult of ( RAlgebra the carrier of X) | [: REAL , ( ContinuousFunctions X):]) . [a, x]) by C0SP1:def 11

      .= (the Mult of ( RAlgebra the carrier of X) . [aa, x]) by FUNCT_1: 49

      .= ((the Mult of ( RAlgebra the carrier of X) | [: REAL , ( BoundedFunctions the carrier of X):]) . [aa, y]) by A1, FUNCT_1: 49

      .= (a * y) by C0SP1:def 11;

    end;



     Lm6: for X be compact non empty TopSpace holds for x1,x2 be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds (x1 * x2) = (y1 * y2)

    proof

      let X be compact non empty TopSpace;

      let x1,x2 be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

      assume

       A1: x1 = y1 & x2 = y2;



      thus (x1 * x2) = ((the multF of ( RAlgebra the carrier of X) || ( ContinuousFunctions X)) . [x1, x2]) by C0SP1:def 6

      .= (the multF of ( RAlgebra the carrier of X) . [x1, x2]) by FUNCT_1: 49

      .= ((the multF of ( RAlgebra the carrier of X) || ( BoundedFunctions the carrier of X)) . [y1, y2]) by A1, FUNCT_1: 49

      .= (y1 * y2) by C0SP1:def 6;

    end;

    registration

      let X be compact non empty TopSpace;

      cluster ( R_Normed_Algebra_of_ContinuousFunctions X) -> Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative;

      coherence

      proof

        ( 1. ( R_Normed_Algebra_of_ContinuousFunctions X)) = ( 1_ ( R_Algebra_of_ContinuousFunctions X));

        hence thesis by Th10;

      end;

    end

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    theorem :: C0SP2:11



     Th11: for X be compact non empty TopSpace holds for F be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds (( Mult_ (( ContinuousFunctions X),( RAlgebra the carrier of X))) . (1,F)) = F

    proof

      let X be compact non empty TopSpace;

      let F be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      set X1 = ( ContinuousFunctions X);

      reconsider f1 = F as Element of X1;



       A1: [jj, f1] in [: REAL , X1:];



      thus (( Mult_ (( ContinuousFunctions X),( RAlgebra the carrier of X))) . (1,F)) = ((the Mult of ( RAlgebra the carrier of X) | [: REAL , X1:]) . (1,f1)) by C0SP1:def 11

      .= (the Mult of ( RAlgebra the carrier of X) . (1,f1)) by A1, FUNCT_1: 49

      .= F by FUNCSDOM: 12;

    end;

    registration

      let X be compact non empty TopSpace;

      cluster ( R_Normed_Algebra_of_ContinuousFunctions X) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th11;

    end

    theorem :: C0SP2:12



     Th12: for X be compact non empty TopSpace holds (X --> 0 ) = ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X))

    proof

      let X be compact non empty TopSpace;

      (X --> 0 ) = ( 0. ( R_Algebra_of_ContinuousFunctions X)) by Th6;

      hence thesis;

    end;



     Lm7: for X be compact non empty TopSpace holds ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X)) = ( 0. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X))

    proof

      let X be compact non empty TopSpace;



      thus ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X)) = (X --> 0 ) by Th12

      .= ( 0. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X)) by C0SP1: 25;

    end;



     Lm8: for X be compact non empty TopSpace holds ( 1. ( R_Normed_Algebra_of_ContinuousFunctions X)) = ( 1. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X))

    proof

      let X be compact non empty TopSpace;



      thus ( 1. ( R_Normed_Algebra_of_ContinuousFunctions X)) = ( 1_ ( R_Algebra_of_ContinuousFunctions X))

      .= (X --> 1) by Th7

      .= ( 1_ ( R_Algebra_of_BoundedFunctions the carrier of X)) by C0SP1: 16

      .= ( 1. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X));

    end;

    theorem :: C0SP2:13

    for X be compact non empty TopSpace holds for F be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||

    proof

      let X be compact non empty TopSpace;

      let F be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      reconsider F1 = F as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;

       ||.F.|| = ||.F1.|| by FUNCT_1: 49;

      hence thesis by C0SP1: 27;

    end;

    theorem :: C0SP2:14

    for X be compact non empty TopSpace holds for F be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds F = ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X)) implies 0 = ||.F.||

    proof

      let X be compact non empty TopSpace;

      let F be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      assume

       A1: F = ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X));

      reconsider F1 = F as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;



       A2: ||.F.|| = ||.F1.|| by FUNCT_1: 49;

      F = (X --> 0 ) by A1, Th12;

      then F1 = ( 0. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X)) by C0SP1: 25;

      hence thesis by A2, C0SP1: 28;

    end;

    theorem :: C0SP2:15



     Th15: for X be compact non empty TopSpace holds for F,G,H be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds for f,g,h be RealMap of X holds (f = F & g = G & h = H implies (H = (F + G) iff for x be Element of X holds (h . x) = ((f . x) + (g . x))))

    proof

      let X be compact non empty TopSpace;

      let F,G,H be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      let f,g,h be RealMap of X;

      reconsider f1 = F, g1 = G, h1 = H as VECTOR of ( R_Algebra_of_ContinuousFunctions X);

      H = (F + G) iff h1 = (f1 + g1);

      hence thesis by Th3;

    end;

    theorem :: C0SP2:16

    for a be Real holds for X be compact non empty TopSpace holds for F,G be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds for f,g be RealMap of X holds (f = F & g = G implies (G = (a * F) iff for x be Element of X holds (g . x) = (a * (f . x))))

    proof

      let a be Real;

      let X be compact non empty TopSpace;

      let F,G be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      let f,g be RealMap of X;

      reconsider f1 = F, g1 = G as VECTOR of ( R_Algebra_of_ContinuousFunctions X);

      G = (a * F) iff g1 = (a * f1);

      hence thesis by Th4;

    end;

    theorem :: C0SP2:17

    for X be compact non empty TopSpace holds for F,G,H be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds for f,g,h be RealMap of X holds (f = F & g = G & h = H implies (H = (F * G) iff for x be Element of X holds (h . x) = ((f . x) * (g . x))))

    proof

      let X be compact non empty TopSpace;

      let F,G,H be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      let f,g,h be RealMap of X;

      reconsider f1 = F, g1 = G, h1 = H as VECTOR of ( R_Algebra_of_ContinuousFunctions X);

      H = (F * G) iff h1 = (f1 * g1);

      hence thesis by Th5;

    end;

    theorem :: C0SP2:18



     Th18: for a be Real holds for X be compact non empty TopSpace holds for F,G be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds ( ||.F.|| = 0 iff F = ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X))) & ( ||.(a * F).|| = ( |.a.| * ||.F.||) & ||.(F + G).|| <= ( ||.F.|| + ||.G.||))

    proof

      let a be Real;

      let X be compact non empty TopSpace;

      let F,G be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      reconsider F1 = F, G1 = G as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;



       A1: ||.F.|| = ||.F1.|| by FUNCT_1: 49;



       A2: ||.G.|| = ||.G1.|| by FUNCT_1: 49;



       A3: ||.(F + G).|| = ||.(F1 + G1).|| by Lm4, Lm3;

       ||.F1.|| = 0 iff F1 = ( 0. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X)) by C0SP1: 32;

      hence ||.F.|| = 0 iff F = ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X)) by Lm7, FUNCT_1: 49;



      thus ||.(a * F).|| = ||.(a * F1).|| by Lm5, Lm3

      .= ( |.a.| * ||.F1.||) by C0SP1: 32

      .= ( |.a.| * ||.F.||) by FUNCT_1: 49;

      thus ||.(F + G).|| <= ( ||.F.|| + ||.G.||) by A1, A2, A3, C0SP1: 32;

    end;

    registration

      let X be compact non empty TopSpace;

      cluster ( R_Normed_Algebra_of_ContinuousFunctions X) -> reflexive discerning RealNormSpace-like;

      coherence

      proof

        set R = ( R_Normed_Algebra_of_ContinuousFunctions X);

        thus ||.( 0. R).|| = 0 by Th18;

        for x,y be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds for a be Real holds ( ||.x.|| = 0 iff x = ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X))) & ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Th18;

        hence thesis by NORMSP_1:def 1;

      end;

    end



     Lm9: for X be compact non empty TopSpace holds for x1,x2 be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds (x1 - x2) = (y1 - y2)

    proof

      let X be compact non empty TopSpace;

      let x1,x2 be Point of ( R_Normed_Algebra_of_ContinuousFunctions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

      assume

       A1: x1 = y1 & x2 = y2;

      ( - x2) = (( - 1) * x2) by RLVECT_1: 16

      .= (( - 1) * y2) by A1, Lm5

      .= ( - y2) by RLVECT_1: 16;

      hence (x1 - x2) = (y1 - y2) by A1, Lm4;

    end;

    theorem :: C0SP2:19

    for X be compact non empty TopSpace holds for F,G,H be Point of ( R_Normed_Algebra_of_ContinuousFunctions X) holds for f,g,h be RealMap of X holds f = F & g = G & h = H implies (H = (F - G) iff (for x be Element of X holds (h . x) = ((f . x) - (g . x))))

    proof

      let X be compact non empty TopSpace;

      let F,G,H be Point of ( R_Normed_Algebra_of_ContinuousFunctions X);

      let f,g,h be RealMap of X;

      assume

       A1: f = F & g = G & h = H;

       A2:

      now

        assume H = (F - G);

        then (H + G) = (F - (G - G)) by RLVECT_1: 29;

        then (H + G) = (F - ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X))) by RLVECT_1: 15;

        then

         A3: (H + G) = F by RLVECT_1: 13;

        now

          let x be Element of X;

          (f . x) = ((h . x) + (g . x)) by A1, A3, Th15;

          hence ((f . x) - (g . x)) = (h . x);

        end;

        hence for x be Element of X holds (h . x) = ((f . x) - (g . x));

      end;

      now

        assume

         A4: for x be Element of X holds (h . x) = ((f . x) - (g . x));

        now

          let x be Element of X;

          (h . x) = ((f . x) - (g . x)) by A4;

          hence ((h . x) + (g . x)) = (f . x);

        end;

        then F = (H + G) by A1, Th15;

        then (F - G) = (H + (G - G)) by RLVECT_1:def 3;

        then (F - G) = (H + ( 0. ( R_Normed_Algebra_of_ContinuousFunctions X))) by RLVECT_1: 15;

        hence (F - G) = H by RLVECT_1: 4;

      end;

      hence thesis by A2;

    end;

    theorem :: C0SP2:20



     Th20: for X be RealBanachSpace, Y be Subset of X, seq be sequence of X st Y is closed & ( rng seq) c= Y & seq is Cauchy_sequence_by_Norm holds seq is convergent & ( lim seq) in Y by LOPBAN_1:def 15, NFCONT_1:def 3;

    theorem :: C0SP2:21



     Th21: for X be compact non empty TopSpace holds for Y be Subset of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = ( ContinuousFunctions X) holds Y is closed

    proof

      let X be compact non empty TopSpace;

      let Y be Subset of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

      assume

       A1: Y = ( ContinuousFunctions X);

      now

        let seq be sequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

        assume

         A2: ( rng seq) c= Y & seq is convergent;

        ( lim seq) in ( BoundedFunctions the carrier of X);

        then

        consider f be Function of the carrier of X, REAL such that

         A3: f = ( lim seq) & (f | the carrier of X) is bounded;

        now

          let z be object;

          assume z in ( BoundedFunctions the carrier of X);

          then ex f be RealMap of X st f = z & (f | the carrier of X) is bounded;

          hence z in ( PFuncs (the carrier of X, REAL )) by PARTFUN1: 45;

        end;

        then ( BoundedFunctions the carrier of X) c= ( PFuncs (the carrier of X, REAL ));

        then

        reconsider H = seq as Functional_Sequence of the carrier of X, REAL by FUNCT_2: 7;



         A4: for p be Real st p > 0 holds ex k be Element of NAT st for n be Element of NAT , x be set st n >= k & x in the carrier of X holds |.(((H . n) . x) - (f . x)).| < p

        proof

          let p be Real;

          assume p > 0 ;

          then

          consider k be Nat such that

           A5: for n be Nat st n >= k holds ||.((seq . n) - ( lim seq)).|| < p by A2, NORMSP_1:def 7;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          take k;

          hereby

            let n be Element of NAT , x be set;

            assume

             A6: n >= k & x in the carrier of X;

            then

             A7: ||.((seq . n) - ( lim seq)).|| < p by A5;

            ((seq . n) - ( lim seq)) in ( BoundedFunctions the carrier of X);

            then

            consider g be RealMap of X such that

             A8: g = ((seq . n) - ( lim seq)) & (g | the carrier of X) is bounded;

            (seq . n) in ( BoundedFunctions the carrier of X);

            then

            consider s be RealMap of X such that

             A9: s = (seq . n) & (s | the carrier of X) is bounded;

            reconsider x0 = x as Element of the carrier of X by A6;



             A10: (g . x0) = ((s . x0) - (f . x0)) by A8, A9, A3, C0SP1: 34;

             |.(g . x0).| <= ||.((seq . n) - ( lim seq)).|| by A8, C0SP1: 26;

            hence |.(((H . n) . x) - (f . x)).| < p by A10, A9, A7, XXREAL_0: 2;

          end;

        end;

        f is continuous

        proof

          for x be Point of X, 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, V be Subset of REAL ;

            set r = (f . x);

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

            then

            consider r0 be Real such that

             A11: 0 < r0 & ].(r - r0), (r + r0).[ c= V by RCOMP_1: 19;

            consider k be Element of NAT such that

             A12: for n be Element of NAT , x be set st n >= k & x in the carrier of X holds |.(((H . n) . x) - (f . x)).| < (r0 / 3) by A4, A11, XREAL_1: 222;



             A13: |.(((H . k) . x) - (f . x)).| < (r0 / 3) by A12;

            k in NAT ;

            then k in ( dom seq) by NORMSP_1: 12;

            then (H . k) in ( rng seq) by FUNCT_1:def 3;

            then (H . k) in Y by A2;

            then

            consider h be continuous RealMap of X such that

             A14: (H . k) = h by A1;

            set r1 = (h . x);

            set G1 = ].(r1 - (r0 / 3)), (r1 + (r0 / 3)).[;



             A15: r1 < (r1 + (r0 / 3)) by A11, XREAL_1: 29, XREAL_1: 222;

            then (r1 - (r0 / 3)) < r1 by XREAL_1: 19;

            then (h . x) in G1 by A15;

            then

            consider W1 be Subset of X such that

             A16: x in W1 & W1 is open & (h .: W1) c= G1 by Th1;

            now

              let x0 be object;

              assume x0 in (f .: W1);

              then

              consider z0 be object such that

               A17: z0 in ( dom f) & z0 in W1 & (f . z0) = x0 by FUNCT_1:def 6;

              (h . z0) in (h .: W1) by A17, FUNCT_2: 35;

              then ((h . x) - (r0 / 3)) < (h . z0) & (h . z0) < ((h . x) + (r0 / 3)) by A16, XXREAL_1: 4;

              then (((h . x) - (r0 / 3)) - (h . x)) < ((h . z0) - (h . x)) & ((h . z0) - (h . x)) < (((h . x) + (r0 / 3)) - (h . x)) by XREAL_1: 9;

              then

               A18: |.((h . z0) - (h . x)).| <= (r0 / 3) by ABSVALUE: 5;



               A19: |.( - ((h . x) - (f . x))).| < (r0 / 3) by A13, A14, COMPLEX1: 52;

               |.((h . z0) - (f . z0)).| < (r0 / 3) by A17, A12, A14;

              then |.( - ((h . z0) - (f . z0))).| < (r0 / 3) by COMPLEX1: 52;

              then ( |.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) < ((r0 / 3) + (r0 / 3)) by A19, XREAL_1: 8;

              then

               A20: (( |.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) + |.((h . z0) - (h . x)).|) < (((r0 / 3) + (r0 / 3)) + (r0 / 3)) by A18, XREAL_1: 8;

               |.((f . z0) - (f . x)).| = |.((((f . z0) - (h . z0)) - ((f . x) - (h . x))) + ((h . z0) - (h . x))).|;

              then

               A21: |.((f . z0) - (f . x)).| <= ( |.(((f . z0) - (h . z0)) - ((f . x) - (h . x))).| + |.((h . z0) - (h . x)).|) by COMPLEX1: 56;

               |.(((f . z0) - (h . z0)) - ((f . x) - (h . x))).| <= ( |.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) by COMPLEX1: 57;

              then ( |.(((f . z0) - (h . z0)) - ((f . x) - (h . x))).| + |.((h . z0) - (h . x)).|) <= (( |.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) + |.((h . z0) - (h . x)).|) by XREAL_1: 6;

              then |.((f . z0) - (f . x)).| <= (( |.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) + |.((h . z0) - (h . x)).|) by A21, XXREAL_0: 2;

              then |.((f . z0) - (f . x)).| < r0 by A20, XXREAL_0: 2;

              then ( - r0) < ((f . z0) - (f . x)) & ((f . z0) - (f . x)) < r0 by SEQ_2: 1;

              then (( - r0) + r) < (((f . z0) - r) + r) & (((f . z0) - r) + r) < (r0 + r) by XREAL_1: 6;

              hence x0 in ].(r - r0), (r + r0).[ by A17;

            end;

            then (f .: W1) c= ].(r - r0), (r + r0).[;

            hence ex W be Subset of X st x in W & W is open & (f .: W) c= V by A16, A11, XBOOLE_1: 1;

          end;

          hence thesis by Th1;

        end;

        hence ( lim seq) in Y by A3, A1;

      end;

      hence thesis by NFCONT_1:def 3;

    end;

    theorem :: C0SP2:22



     Th22: for X be compact non empty TopSpace holds for seq be sequence of ( R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds seq is convergent

    proof

      let X be compact non empty TopSpace;

      let vseq be sequence of ( R_Normed_Algebra_of_ContinuousFunctions X);

      assume

       A1: vseq is Cauchy_sequence_by_Norm;



       A2: for x be object st x in ( ContinuousFunctions X) holds x in ( BoundedFunctions the carrier of X) by Lm1;

      then ( ContinuousFunctions X) c= ( BoundedFunctions the carrier of X);

      then ( rng vseq) c= ( BoundedFunctions the carrier of X);

      then

      reconsider vseq1 = vseq as sequence of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by FUNCT_2: 6;

      now

        let e be Real such that

         A3: e > 0 ;

        consider k be Nat such that

         A4: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A3, RSSPACE3: 8;

        take k;

        let n,m be Nat;

        assume n >= k & m >= k;

        then ||.((vseq . n) - (vseq . m)).|| < e by A4;

        hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Lm9, Lm3;

      end;

      then

       A5: vseq1 is Cauchy_sequence_by_Norm by RSSPACE3: 8;

      then

       A6: vseq1 is convergent by C0SP1: 35;

      reconsider Y = ( ContinuousFunctions X) as Subset of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by A2, TARSKI:def 3;



       A7: ( rng vseq) c= ( ContinuousFunctions X);

      Y is closed by Th21;

      then

      reconsider tv = ( lim vseq1) as Point of ( R_Normed_Algebra_of_ContinuousFunctions X) by A7, A5, Th20;

      for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds ||.((vseq . n) - tv).|| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

         A8: for n be Nat st n >= k holds ||.((vseq1 . n) - ( lim vseq1)).|| < e by A6, NORMSP_1:def 7;

        take k;

        now

          let n be Nat;

          assume n >= k;

          then ||.((vseq1 . n) - ( lim vseq1)).|| < e by A8;

          hence ||.((vseq . n) - tv).|| < e by Lm9, Lm3;

        end;

        hence for n be Nat st n >= k holds ||.((vseq . n) - tv).|| < e;

      end;

      hence thesis by NORMSP_1:def 6;

    end;

    registration

      let X be compact non empty TopSpace;

      cluster ( R_Normed_Algebra_of_ContinuousFunctions X) -> complete;

      coherence

      proof

        for seq be sequence of ( R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th22;

        hence thesis by LOPBAN_1:def 15;

      end;

    end

    registration

      let X be compact non empty TopSpace;

      cluster ( R_Normed_Algebra_of_ContinuousFunctions X) -> Banach_Algebra-like;

      coherence

      proof

        set B = ( R_Normed_Algebra_of_ContinuousFunctions X);

         A1:

        now

          let f,g be Element of B;

          reconsider f1 = f, g1 = g as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;



           A2: ||.f.|| = ||.f1.|| & ||.g.|| = ||.g1.|| & ||.(f * g).|| = ||.(f1 * g1).|| by Lm6, Lm3;

          thus ||.(f * g).|| <= ( ||.f.|| * ||.g.||) by A2, LOPBAN_2:def 9;

        end;



         A3: ||.( 1. B).|| = ||.( 1. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X)).|| by Lm8, Lm3

        .= 1 by LOPBAN_2:def 10;

         A4:

        now

          let a be Real, f,g be Element of B;

          reconsider f1 = f, g1 = g as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;



           A5: (a * g1) = (a * g) by Lm5;



           A6: (f * g) = (f1 * g1) by Lm6;

          (a * (f * g)) = (a * (f1 * g1)) by A6, Lm5;

          then (a * (f * g)) = (f1 * (a * g1)) by LOPBAN_2:def 11;

          hence (a * (f * g)) = (f * (a * g)) by A5, Lm6;

        end;

        now

          let f,g,h be Element of B;

          reconsider f1 = f, g1 = g, h1 = h as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;



           A7: (g + h) = (g1 + h1) by Lm4;



           A8: (g * f) = (g1 * f1) & (h * f) = (h1 * f1) by Lm6;



          thus ((g + h) * f) = ((g1 + h1) * f1) by Lm6, A7

          .= ((g1 * f1) + (h1 * f1)) by VECTSP_1:def 3

          .= ((g * f) + (h * f)) by Lm4, A8;

        end;

        then B is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 left-distributive left_unital complete Normed_Algebra by A1, A3, A4, LOPBAN_2:def 9, LOPBAN_2:def 10, LOPBAN_2:def 11, VECTSP_1:def 3;

        hence thesis;

      end;

    end

    begin

    theorem :: C0SP2:23



     Th23: for X be non empty TopSpace holds for f,g be RealMap of X holds ( support (f + g)) c= (( support f) \/ ( support g))

    proof

      let X be non empty TopSpace;

      let f,g be RealMap of X;

      set CX = the carrier of X;

      reconsider h = (f + g) as RealMap of X;



       A1: ( dom f) = CX & ( dom g) = CX & ( dom h) = CX by FUNCT_2:def 1;

      now

        let x be object;

        assume

         A2: x in ((CX \ ( support f)) /\ (CX \ ( support g)));

        then x in (CX \ ( support f)) & x in (CX \ ( support g)) by XBOOLE_0:def 4;

        then x in CX & not x in ( support f) & x in CX & not x in ( support g) by XBOOLE_0:def 5;

        then

         A3: x in CX & (f . x) = 0 & (g . x) = 0 by PRE_POLY:def 7;



         A4: ((f + g) . x) = ( 0 + 0 ) by A3, VALUED_1: 1;

         not x in ( support (f + g)) by A4, PRE_POLY:def 7;

        hence x in (CX \ ( support (f + g))) by A2, XBOOLE_0:def 5;

      end;

      then ((CX \ ( support f)) /\ (CX \ ( support g))) c= (CX \ ( support (f + g)));

      then (CX \ (( support f) \/ ( support g))) c= (CX \ ( support (f + g))) by XBOOLE_1: 53;

      then (CX \ (CX \ ( support (f + g)))) c= (CX \ (CX \ (( support f) \/ ( support g)))) by XBOOLE_1: 34;

      then (CX /\ ( support (f + g))) c= (CX \ (CX \ (( support f) \/ ( support g)))) by XBOOLE_1: 48;

      then (CX /\ ( support (f + g))) c= (CX /\ (( support f) \/ ( support g))) by XBOOLE_1: 48;

      then ( support (f + g)) c= (CX /\ (( support f) \/ ( support g))) by A1, PRE_POLY: 37, XBOOLE_1: 28;

      then ( support (f + g)) c= ((CX /\ ( support f)) \/ (CX /\ ( support g))) by XBOOLE_1: 23;

      then ( support (f + g)) c= (( support f) \/ (CX /\ ( support g))) by A1, PRE_POLY: 37, XBOOLE_1: 28;

      hence thesis by A1, PRE_POLY: 37, XBOOLE_1: 28;

    end;

    theorem :: C0SP2:24



     Th24: for X be non empty TopSpace holds for a be Real, f be RealMap of X holds ( support (a (#) f)) c= ( support f)

    proof

      let X be non empty TopSpace;

      let a be Real, f be RealMap of X;

      set CX = the carrier of X;

      reconsider h = (a (#) f) as RealMap of X;

      now

        let x be object;

        assume x in ( support (a (#) f));

        then ((a (#) f) . x) <> 0 by PRE_POLY:def 7;

        then

         A1: (a * (f . x)) <> 0 by VALUED_1: 6;

        (f . x) <> 0 by A1;

        hence x in ( support f) by PRE_POLY:def 7;

      end;

      hence thesis;

    end;

    theorem :: C0SP2:25

    for X be non empty TopSpace holds for f,g be RealMap of X holds ( support (f (#) g)) c= (( support f) \/ ( support g))

    proof

      let X be non empty TopSpace;

      let f,g be RealMap of X;

      set CX = the carrier of X;

      reconsider h = (f (#) g) as RealMap of X;



       A1: ( dom f) = CX & ( dom g) = CX & ( dom h) = CX by FUNCT_2:def 1;

      now

        let x be object;

        assume

         A2: x in ((CX \ ( support f)) /\ (CX \ ( support g)));

        then x in (CX \ ( support f)) & x in (CX \ ( support g)) by XBOOLE_0:def 4;

        then x in CX & not x in ( support f) & x in CX & not x in ( support g) by XBOOLE_0:def 5;

        then

         A3: x in CX & (f . x) = 0 & (g . x) = 0 by PRE_POLY:def 7;



         A4: ((f (#) g) . x) = ( 0 * 0 ) by A3, VALUED_1: 5;

         not x in ( support (f (#) g)) by A4, PRE_POLY:def 7;

        hence x in (CX \ ( support (f (#) g))) by A2, XBOOLE_0:def 5;

      end;

      then ((CX \ ( support f)) /\ (CX \ ( support g))) c= (CX \ ( support (f (#) g)));

      then (CX \ (( support f) \/ ( support g))) c= (CX \ ( support (f (#) g))) by XBOOLE_1: 53;

      then (CX \ (CX \ ( support (f (#) g)))) c= (CX \ (CX \ (( support f) \/ ( support g)))) by XBOOLE_1: 34;

      then (CX /\ ( support (f (#) g))) c= (CX \ (CX \ (( support f) \/ ( support g)))) by XBOOLE_1: 48;

      then (CX /\ ( support (f (#) g))) c= (CX /\ (( support f) \/ ( support g))) by XBOOLE_1: 48;

      then ( support (f (#) g)) c= (CX /\ (( support f) \/ ( support g))) by A1, PRE_POLY: 37, XBOOLE_1: 28;

      then ( support (f (#) g)) c= ((CX /\ ( support f)) \/ (CX /\ ( support g))) by XBOOLE_1: 23;

      then ( support (f (#) g)) c= (( support f) \/ (CX /\ ( support g))) by A1, PRE_POLY: 37, XBOOLE_1: 28;

      hence thesis by A1, PRE_POLY: 37, XBOOLE_1: 28;

    end;

    begin

    definition

      let X be non empty TopSpace;

      :: C0SP2:def6

      func C_0_Functions (X) -> non empty Subset of ( RealVectSpace the carrier of X) equals { f where f be RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) };

      correctness

      proof



         A1: { f where f be RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) } c= ( Funcs (the carrier of X, REAL ))

        proof

          for x be object st x in { f where f be RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) } holds x in ( Funcs (the carrier of X, REAL ))

          proof

            let x be object;

            assume x in { f where f be RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) };

            then ex f be RealMap of X st x = f & f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y));

            hence x in ( Funcs (the carrier of X, REAL )) by FUNCT_2: 8;

          end;

          hence thesis;

        end;

        { f where f be RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) } is non empty

        proof

          set g = (the carrier of X --> ( In ( 0 , REAL )));

          reconsider g as RealMap of X;



           A2: g is continuous

          proof

            for P be Subset of REAL st P is closed holds (g " P) is closed

            proof

              let P be Subset of REAL such that P is closed;

              set F = (the carrier of X --> 0 ), H = the carrier of X;

              set HX = ( [#] X);

              per cases ;

                suppose 0 in P;

                then (g " P) = HX by FUNCOP_1: 14;

                hence (g " P) is closed;

              end;

                suppose not 0 in P;

                then (F " P) = ( {} X) by FUNCOP_1: 16;

                hence (g " P) is closed;

              end;

            end;

            hence thesis;

          end;



           A3: ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support g) holds ( Cl A) is Subset of Y))

          proof

            set S = the compact non empty Subset of X;



             A4: for A be Subset of X st A = ( support g) holds ( Cl A) is Subset of S

            proof

              let A be Subset of X;

              assume

               A5: A = ( support g);



               A6: A = {}

              proof

                assume

                 A7: not thesis;

                set p = the Element of ( support g);



                 A8: p in A by A7, A5;

                (g . p) <> 0 by A5, A7, PRE_POLY:def 7;

                hence contradiction by A8, FUNCOP_1: 7;

              end;

              ( Cl A) = ( {} X) by A6, PRE_TOPC: 22;

              hence thesis by XBOOLE_1: 2;

            end;

            thus thesis by A4;

          end;

          g in { f where f be RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) } by A2, A3;

          hence thesis;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: C0SP2:26

    for X be non empty TopSpace holds ( C_0_Functions X) is non empty Subset of ( RAlgebra the carrier of X);



     Lm10: for X be non empty TopSpace holds for v,u be Element of ( RAlgebra the carrier of X) st v in ( C_0_Functions X) & u in ( C_0_Functions X) holds (v + u) in ( C_0_Functions X)

    proof

      let X be non empty TopSpace;

      set W = ( C_0_Functions X);

      set V = ( RAlgebra the carrier of X);

      let u,v be Element of V such that

       A1: u in W & v in W;

      consider u1 be RealMap of X such that

       A2: u1 = u & u1 is continuous & (ex Y1 be non empty Subset of X st Y1 is compact & (for A1 be Subset of X st A1 = ( support u1) holds ( Cl A1) is Subset of Y1)) by A1;

      consider Y1 be non empty Subset of X such that

       A3: (Y1 is compact & (for A1 be Subset of X st A1 = ( support u1) holds ( Cl A1) is Subset of Y1)) by A2;

      consider v1 be RealMap of X such that

       A4: v1 = v & v1 is continuous & (ex Y2 be non empty Subset of X st Y2 is compact & (for A2 be Subset of X st A2 = ( support v1) holds ( Cl A2) is Subset of Y2)) by A1;

      consider Y2 be non empty Subset of X such that

       A5: (Y2 is compact & (for A2 be Subset of X st A2 = ( support v1) holds ( Cl A2) is Subset of Y2)) by A4;



       A6: u in ( ContinuousFunctions X) by A2;



       A7: v in ( ContinuousFunctions X) by A4;

      (v + u) in ( ContinuousFunctions X) by A6, A7, IDEAL_1:def 1;

      then

      consider fvu be continuous RealMap of X such that

       A8: (v + u) = fvu;



       A9: (Y1 \/ Y2) is compact by A3, A5, COMPTS_1: 10;



       A10: ( dom u1) = the carrier of X & ( dom v1) = the carrier of X by FUNCT_2:def 1;

      reconsider A1 = ( support u1), A2 = ( support v1) as Subset of X by A10, PRE_POLY: 37;



       A11: (( dom v1) /\ ( dom u1)) = (the carrier of X /\ ( dom u1)) by FUNCT_2:def 1

      .= (the carrier of X /\ the carrier of X) by FUNCT_2:def 1

      .= the carrier of X;



       A12: ( dom (v1 + u1)) = (( dom v1) /\ ( dom u1)) by VALUED_1:def 1;

      reconsider A1 = ( support u1), A2 = ( support v1) as Subset of X by A10, PRE_POLY: 37;

      reconsider A3 = ( support (v1 + u1)) as Subset of X by A12, A11, PRE_POLY: 37;

      ( Cl A3) c= ( Cl (A2 \/ A1)) by Th23, PRE_TOPC: 19;

      then

       A13: ( Cl A3) c= (( Cl A2) \/ ( Cl A1)) by PRE_TOPC: 20;



       A14: ( Cl A1) is Subset of Y1 by A3;

      ( Cl A2) is Subset of Y2 by A5;

      then (( Cl A2) \/ ( Cl A1)) c= (Y2 \/ Y1) by A14, XBOOLE_1: 13;

      then

       A15: for A3 be Subset of X st A3 = ( support (v1 + u1)) holds ( Cl A3) is Subset of (Y2 \/ Y1) by A13, XBOOLE_1: 1;

      reconsider vv1 = v as Element of ( Funcs (the carrier of X, REAL ));

      reconsider uu1 = u as Element of ( Funcs (the carrier of X, REAL ));

      reconsider fvu1 = (v + u) as Element of ( Funcs (the carrier of X, REAL ));



       A16: ( dom fvu1) = the carrier of X by FUNCT_2:def 1;

      for c be object st c in ( dom fvu1) holds (fvu1 . c) = ((v1 . c) + (u1 . c)) by A2, A4, FUNCSDOM: 1;

      then fvu1 = (v1 + u1) by A16, A11, VALUED_1:def 1;

      hence thesis by A8, A9, A15;

    end;



     Lm11: for X be non empty TopSpace holds for a be Real, u be Element of ( RAlgebra the carrier of X) st u in ( C_0_Functions X) holds (a * u) in ( C_0_Functions X)

    proof

      let X be non empty TopSpace;

      set W = ( C_0_Functions X);

      set V = ( RAlgebra the carrier of X);

      let a be Real;

      let u be Element of V;

      assume

       A1: u in W;

      consider u1 be RealMap of X such that

       A2: u1 = u & u1 is continuous & (ex Y1 be non empty Subset of X st Y1 is compact & (for A1 be Subset of X st A1 = ( support u1) holds ( Cl A1) is Subset of Y1)) by A1;

      consider Y1 be non empty Subset of X such that

       A3: (Y1 is compact & (for A1 be Subset of X st A1 = ( support u1) holds ( Cl A1) is Subset of Y1)) by A2;



       A4: u in ( ContinuousFunctions X) by A2;

      reconsider aa = a as Real;

      (aa * u) in ( ContinuousFunctions X) by A4, C0SP1:def 10;

      then

      consider fau be continuous RealMap of X such that

       A5: fau = (a * u);



       A6: ( dom u1) = the carrier of X by FUNCT_2:def 1;

      then

      reconsider A1 = ( support u1) as Subset of X by PRE_POLY: 37;



       A7: ( dom u1) = the carrier of X by FUNCT_2:def 1;



       A8: ( dom (a (#) u1)) = ( dom u1) by VALUED_1:def 5;

      reconsider A1 = ( support u1) as Subset of X by A6, PRE_POLY: 37;

      reconsider A3 = ( support (a (#) u1)) as Subset of X by A8, A7, PRE_POLY: 37;



       A9: ( Cl A1) is Subset of Y1 by A3;

      ( Cl A3) c= ( Cl A1) by Th24, PRE_TOPC: 19;

      then

       A10: for A3 be Subset of X st A3 = ( support (a (#) u1)) holds ( Cl A3) is Subset of Y1 by A9, XBOOLE_1: 1;

      reconsider uu1 = u as Element of ( Funcs (the carrier of X, REAL ));

      reconsider fau1 = (a * u) as Element of ( Funcs (the carrier of X, REAL ));



       A11: ( dom fau1) = the carrier of X by FUNCT_2:def 1;



       A12: ( dom u1) = the carrier of X by FUNCT_2:def 1;

      for c be object st c in ( dom fau1) holds (fau1 . c) = (a * (u1 . c)) by A2, FUNCSDOM: 4;

      then fau1 = (a (#) u1) by A11, A12, VALUED_1:def 5;

      hence thesis by A3, A10, A5;

    end;



     Lm12: for X be non empty TopSpace holds for u be Element of ( RAlgebra the carrier of X) st u in ( C_0_Functions X) holds ( - u) in ( C_0_Functions X)

    proof

      let X be non empty TopSpace;

      set W = ( C_0_Functions X);

      set V = ( RAlgebra the carrier of X);

      let u be Element of V;

      assume

       A1: u in W;

      set a = ( - 1);

      ( RAlgebra the carrier of X) is RealLinearSpace by C0SP1: 7;

      then ( - u) = (a * u) by RLVECT_1: 16;

      hence thesis by Lm11, A1;

    end;

    theorem :: C0SP2:27

    for X be non empty TopSpace holds for W be non empty Subset of ( RAlgebra the carrier of X) st W = ( C_0_Functions X) holds W is additively-linearly-closed

    proof

      let X be non empty TopSpace;

      let W be non empty Subset of ( RAlgebra the carrier of X);

      assume

       A1: W = ( C_0_Functions X);

      set V = ( RAlgebra the carrier of X);

      for v,u be Element of V st v in W & u in W holds (v + u) in W by A1, Lm10;

      then

       A2: W is add-closed by IDEAL_1:def 1;

      for v be Element of V st v in W holds ( - v) in W by A1, Lm12;

      then

       A3: W is having-inverse;

      for a be Real, u be Element of V st u in W holds (a * u) in W by A1, Lm11;

      hence W is additively-linearly-closed by A2, A3;

    end;

    theorem :: C0SP2:28



     Th28: for X be non empty TopSpace holds ( C_0_Functions X) is linearly-closed

    proof

      let X be non empty TopSpace;

      set Y = ( C_0_Functions X);

      set V = ( RealVectSpace the carrier of X);



       A1: for v,u be VECTOR of V st v in Y & u in Y holds (v + u) in Y

      proof

        let v,u be VECTOR of V;

        assume

         A2: v in Y & u in Y;

        reconsider v1 = v, u1 = u as Element of ( Funcs (the carrier of X, REAL ));

        reconsider v2 = v, u2 = u as VECTOR of ( RAlgebra the carrier of X);

        (v2 + u2) in Y by A2, Lm10;

        hence thesis;

      end;

      for a be Real, v be Element of V st v in Y holds (a * v) in Y

      proof

        let a be Real, v be VECTOR of V;

        assume

         A3: v in Y;

        reconsider v1 = v as Element of ( Funcs (the carrier of X, REAL ));

        reconsider v2 = v as VECTOR of ( RAlgebra the carrier of X);

        (a * v2) in Y by A3, Lm11;

        hence thesis;

      end;

      hence thesis by A1, RLSUB_1:def 1;

    end;

    registration

      let X be non empty TopSpace;

      cluster ( C_0_Functions X) -> non empty linearly-closed;

      correctness by Th28;

    end

    definition

      let X be non empty TopSpace;

      :: C0SP2:def7

      func R_VectorSpace_of_C_0_Functions (X) -> RealLinearSpace equals RLSStruct (# ( C_0_Functions X), ( Zero_ (( C_0_Functions X),( RealVectSpace the carrier of X))), ( Add_ (( C_0_Functions X),( RealVectSpace the carrier of X))), ( Mult_ (( C_0_Functions X),( RealVectSpace the carrier of X))) #);

      correctness by RSSPACE: 11;

    end

    theorem :: C0SP2:29

    for X be non empty TopSpace holds ( R_VectorSpace_of_C_0_Functions X) is Subspace of ( RealVectSpace the carrier of X) by RSSPACE: 11;

    theorem :: C0SP2:30



     Th30: for X be non empty TopSpace holds for x be set st x in ( C_0_Functions X) holds x in ( BoundedFunctions the carrier of X)

    proof

      let X be non empty TopSpace;

      let x be set such that

       A1: x in ( C_0_Functions X);

      consider f be RealMap of X such that

       A2: f = x & f is continuous & (ex Y be non empty Subset of X st Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) by A1;

      consider Y be non empty Subset of X such that

       A3: (Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) by A2;

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

      then

      reconsider A = ( support f) as Subset of X by PRE_POLY: 37;

      reconsider Y1 = (f .: Y) as non empty real-bounded Subset of REAL by A2, A3, JORDAN_A: 1, RCOMP_1: 10;



       A4: Y1 c= [.( inf Y1), ( sup Y1).] by XXREAL_2: 69;

      reconsider r1 = ( inf Y1), r2 = ( sup Y1) as Real;

      consider r be Real such that

       A5: r = (( |.r1.| + |.r2.|) + 1);

      for p be Element of Y holds r > 0 & ( - r) < (f . p) & (f . p) < r

      proof

        let p be Element of Y;

        (f . p) in Y1 by FUNCT_2: 35;

        then (f . p) in [.r1, r2.] by A4;

        then

        consider r3 be Real such that

         A6: r3 = (f . p) & r1 <= r3 & r3 <= r2;



         A7: |.r1.| >= 0 & |.r2.| >= 0 by COMPLEX1: 46;

        ( - |.r1.|) <= r1 by ABSVALUE: 4;

        then (( - |.r1.|) - |.r2.|) <= (r1 - 0 ) by A7, XREAL_1: 13;

        then ((( - |.r1.|) - |.r2.|) - 1) < (r1 - 0 ) by XREAL_1: 15;

        then

         A8: ( - r) < r1 by A5;

        r2 <= |.r2.| by ABSVALUE: 4;

        then (r2 + 0 ) <= ( |.r2.| + |.r1.|) by A7, XREAL_1: 7;

        then r2 < r by A5, XREAL_1: 8;

        hence thesis by A6, A8, XXREAL_0: 2;

      end;

      then

      consider r be Real such that

       A9: for p be Element of Y holds r > 0 & ( - r) < (f . p) & (f . p) < r;

      for x be Point of X holds (( - r) < (f . x) & (f . x) < r)

      proof

        let x be Point of X;

        per cases by XBOOLE_0:def 5;

          suppose

           A10: x in (the carrier of X \ Y);



           A11: ( Cl A) is Subset of Y by A3;

          ( support f) c= ( Cl A) by PRE_TOPC: 18;

          then ( support f) c= Y by A11, XBOOLE_1: 1;

          then not x in ( support f) by A10, XBOOLE_0:def 5;

          then

           A12: (f . x) = 0 by PRE_POLY:def 7;

          (( - 1) * r) < (( - 1) * 0 ) by A9, XREAL_1: 69;

          hence ( - r) < (f . x) & (f . x) < r by A12;

        end;

          suppose x in Y;

          hence thesis by A9;

        end;

      end;

      then

      consider s1 be Real such that

       A13: for x be Point of X holds (( - s1) < (f . x) & (f . x) < s1);

      for y be object st y in (the carrier of X /\ ( dom f)) holds (f . y) <= s1 by A13;

      then

       A14: (f | the carrier of X) is bounded_above by RFUNCT_1: 70;

      for y be object st y in (the carrier of X /\ ( dom f)) holds ( - s1) <= (f . y) by A13;

      then

       A15: (f | the carrier of X) is bounded_below by RFUNCT_1: 71;

      (the carrier of X /\ the carrier of X) = the carrier of X;

      then (f | the carrier of X) is bounded by A14, A15, RFUNCT_1: 75;

      hence x in ( BoundedFunctions the carrier of X) by A2;

    end;

    definition

      let X be non empty TopSpace;

      :: C0SP2:def8

      func C_0_FunctionsNorm X -> Function of ( C_0_Functions X), REAL equals (( BoundedFunctionsNorm the carrier of X) | ( C_0_Functions X));

      correctness

      proof

        for x be object st x in ( C_0_Functions X) holds x in ( BoundedFunctions the carrier of X) by Th30;

        then ( C_0_Functions X) c= ( BoundedFunctions the carrier of X);

        hence thesis by FUNCT_2: 32;

      end;

    end

    definition

      let X be non empty TopSpace;

      :: C0SP2:def9

      func R_Normed_Space_of_C_0_Functions (X) -> non empty NORMSTR equals NORMSTR (# ( C_0_Functions X), ( Zero_ (( C_0_Functions X),( RealVectSpace the carrier of X))), ( Add_ (( C_0_Functions X),( RealVectSpace the carrier of X))), ( Mult_ (( C_0_Functions X),( RealVectSpace the carrier of X))), ( C_0_FunctionsNorm X) #);

      correctness ;

    end

    registration

      let X be non empty TopSpace;

      cluster ( R_Normed_Space_of_C_0_Functions X) -> strict non empty;

      correctness ;

    end

    theorem :: C0SP2:31

    for X be non empty TopSpace holds for x be set st x in ( C_0_Functions X) holds x in ( ContinuousFunctions X)

    proof

      let X be non empty TopSpace;

      let x be set such that

       A1: x in ( C_0_Functions X);

      consider f be RealMap of X such that

       A2: f = x & f is continuous & (ex Y be non empty Subset of X st Y is compact & (for A be Subset of X st A = ( support f) holds ( Cl A) is Subset of Y)) by A1;

      thus thesis by A2;

    end;

    theorem :: C0SP2:32



     Th32: for X be non empty TopSpace holds ( 0. ( R_VectorSpace_of_C_0_Functions X)) = (X --> 0 )

    proof

      let X be non empty TopSpace;



       A1: ( R_VectorSpace_of_C_0_Functions X) is Subspace of ( RealVectSpace the carrier of X) by RSSPACE: 11;

      ( 0. ( RealVectSpace the carrier of X)) = (X --> 0 );

      hence thesis by A1, RLSUB_1: 11;

    end;

    theorem :: C0SP2:33



     Th33: for X be non empty TopSpace holds ( 0. ( R_Normed_Space_of_C_0_Functions X)) = (X --> 0 )

    proof

      let X be non empty TopSpace;

      ( 0. ( R_Normed_Space_of_C_0_Functions X)) = ( 0. ( R_VectorSpace_of_C_0_Functions X))

      .= (X --> 0 ) by Th32;

      hence thesis;

    end;



     Lm13: for X be non empty TopSpace holds for x1,x2 be Point of ( R_Normed_Space_of_C_0_Functions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds (x1 + x2) = (y1 + y2)

    proof

      let X be non empty TopSpace;

      let x1,x2 be Point of ( R_Normed_Space_of_C_0_Functions X), y1,y2 be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

      assume

       A1: x1 = y1 & x2 = y2;



      thus (x1 + x2) = ((the addF of ( RealVectSpace the carrier of X) || ( C_0_Functions X)) . [x1, x2]) by RSSPACE:def 8

      .= (the addF of ( RAlgebra the carrier of X) . [x1, x2]) by FUNCT_1: 49

      .= ((the addF of ( RAlgebra the carrier of X) || ( BoundedFunctions the carrier of X)) . [y1, y2]) by A1, FUNCT_1: 49

      .= (y1 + y2) by C0SP1:def 5;

    end;



     Lm14: for X be non empty TopSpace holds for a be Real, x be Point of ( R_Normed_Space_of_C_0_Functions X), y be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds (a * x) = (a * y)

    proof

      let X be non empty TopSpace;

      let a be Real, x be Point of ( R_Normed_Space_of_C_0_Functions X), y be Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

      assume

       A1: x = y;

      reconsider aa = a as Element of REAL by XREAL_0:def 1;



      thus (a * x) = ((the Mult of ( RAlgebra the carrier of X) | [: REAL , ( C_0_Functions X):]) . [a, x]) by RSSPACE:def 9

      .= (the Mult of ( RAlgebra the carrier of X) . [aa, x]) by FUNCT_1: 49

      .= ((the Mult of ( RAlgebra the carrier of X) | [: REAL , ( BoundedFunctions the carrier of X):]) . [aa, y]) by A1, FUNCT_1: 49

      .= (a * y) by C0SP1:def 11;

    end;

    theorem :: C0SP2:34



     Th34: for a be Real holds for X be non empty TopSpace holds for F,G be Point of ( R_Normed_Space_of_C_0_Functions X) holds ( ||.F.|| = 0 iff F = ( 0. ( R_Normed_Space_of_C_0_Functions X))) & ||.(a * F).|| = ( |.a.| * ||.F.||) & ||.(F + G).|| <= ( ||.F.|| + ||.G.||)

    proof

      let a be Real;

      let X be non empty TopSpace;

      let F,G be Point of ( R_Normed_Space_of_C_0_Functions X);



       A1: ||.F.|| = 0 iff F = ( 0. ( R_Normed_Space_of_C_0_Functions X))

      proof

        reconsider FB = F as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;



         A2: ( 0. ( R_Normed_Space_of_C_0_Functions X)) = (X --> 0 ) by Th33;

         ||.FB.|| = 0 iff FB = ( 0. ( R_Normed_Algebra_of_BoundedFunctions the carrier of X)) by C0SP1: 32;

        hence thesis by A2, C0SP1: 25, FUNCT_1: 49;

      end;



       A3: ||.(a * F).|| = ( |.a.| * ||.F.||)

      proof

        reconsider FB = F as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;



         A4: ||.FB.|| = ||.F.|| by FUNCT_1: 49;



         A5: (a * FB) = (a * F) by Lm14;

        reconsider aFB = (a * FB) as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

        reconsider aF = (a * F) as Point of ( R_Normed_Space_of_C_0_Functions X);

         ||.aFB.|| = ||.aF.|| by A5, FUNCT_1: 49;

        hence thesis by A4, C0SP1: 32;

      end;

       ||.(F + G).|| <= ( ||.F.|| + ||.G.||)

      proof

        reconsider FB = F, GB = G as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;



         A6: ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| by FUNCT_1: 49;

        (FB + GB) = (F + G) by Lm13;

        then

         A7: ||.(FB + GB).|| = ||.(F + G).|| by FUNCT_1: 49;

        reconsider aFB = (FB + GB) as Point of ( R_Normed_Algebra_of_BoundedFunctions the carrier of X);

        reconsider aF = F, aG = G as Point of ( R_Normed_Space_of_C_0_Functions X);

        thus thesis by A7, A6, C0SP1: 32;

      end;

      hence thesis by A1, A3;

    end;

    theorem :: C0SP2:35



     Th35: for X be non empty TopSpace holds ( R_Normed_Space_of_C_0_Functions X) is RealNormSpace-like

    proof

      let X be non empty TopSpace;

      for x,y be Point of ( R_Normed_Space_of_C_0_Functions X) holds for a be Real holds ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Th34;

      hence thesis by NORMSP_1:def 1;

    end;

    registration

      let X be non empty TopSpace;

      cluster ( R_Normed_Space_of_C_0_Functions X) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence

      proof



         A1: ( R_VectorSpace_of_C_0_Functions X) is RealLinearSpace;



         A2: for x be Point of ( R_Normed_Space_of_C_0_Functions X) st ||.x.|| = 0 holds x = ( 0. ( R_Normed_Space_of_C_0_Functions X)) by Th34;

         ||.( 0. ( R_Normed_Space_of_C_0_Functions X)).|| = 0 by Th34;

        hence thesis by A1, A2, Th35, RSSPACE3: 2;

      end;

    end

    theorem :: C0SP2:36

    for X be non empty TopSpace holds ( R_Normed_Space_of_C_0_Functions X) is RealNormSpace;