c0sp1.miz



    begin

    definition

      let V be non empty addLoopStr;

      let V1 be Subset of V;

      :: C0SP1:def1

      attr V1 is having-inverse means for v be Element of V st v in V1 holds ( - v) in V1;

    end

    definition

      let V be non empty addLoopStr;

      let V1 be Subset of V;

      :: C0SP1:def2

      attr V1 is additively-closed means V1 is add-closed having-inverse;

    end

    

     Lm1: for V be non empty addLoopStr holds ( [#] V) is add-closed

    proof

      let V be non empty addLoopStr;

      for v,u be Element of V st v in ( [#] V) & u in ( [#] V) holds (v + u) in ( [#] V);

      hence thesis by IDEAL_1:def 1;

    end;

    registration

      let V be non empty addLoopStr;

      cluster ( [#] V) -> add-closed having-inverse;

      correctness by Lm1;

    end

    registration

      let V be non empty doubleLoopStr;

      cluster additively-closed -> add-closed having-inverse for Subset of V;

      coherence ;

      cluster add-closed having-inverse -> additively-closed for Subset of V;

      coherence ;

    end

    registration

      let V be non empty addLoopStr;

      cluster add-closed having-inverse non empty for Subset of V;

      correctness

      proof

        take ( [#] V);

        thus thesis;

      end;

    end

    definition

      let V be Ring;

      :: C0SP1:def3

      mode Subring of V -> Ring means

      : Def3: the carrier of it c= the carrier of V & the addF of it = (the addF of V || the carrier of it ) & the multF of it = (the multF of V || the carrier of it ) & ( 1. it ) = ( 1. V) & ( 0. it ) = ( 0. V);

      existence

      proof

        take V;

        thus thesis by RELSET_1: 19;

      end;

    end

    reserve X for non empty set;

    reserve x for Element of X;

    reserve d1,d2 for Element of X;

    reserve A for BinOp of X;

    reserve M for Function of [:X, X:], X;

    reserve V for Ring;

    reserve V1 for Subset of V;

    theorem :: C0SP1:1

    

     Th1: V1 = X & A = (the addF of V || V1) & M = (the multF of V || V1) & d1 = ( 1. V) & d2 = ( 0. V) & V1 is having-inverse implies doubleLoopStr (# X, A, M, d1, d2 #) is Subring of V

    proof

      assume that

       A1: V1 = X and

       A2: A = (the addF of V || V1) and

       A3: M = (the multF of V || V1) and

       A4: d1 = ( 1. V) and

       A5: d2 = ( 0. V) and

       A6: for v be Element of V st v in V1 holds ( - v) in V1;

      reconsider W = doubleLoopStr (# X, A, M, d1, d2 #) as non empty doubleLoopStr;

       A7:

      now

        let a,x be Element of W;

        (a * x) = (the multF of V . [a, x]) by A1, A3, FUNCT_1: 49;

        hence (a * x) = (the multF of V . (a,x));

      end;

       A8:

      now

        let x,y be Element of W;

        (x + y) = (the addF of V . [x, y]) by A1, A2, FUNCT_1: 49;

        hence (x + y) = (the addF of V . (x,y));

      end;

      

       A9: W is Abelian add-associative right_zeroed right_complementable associative well-unital distributive

      proof

        set MV = the multF of V;

        set Av = the addF of V;

        hereby

          let x,y be Element of W;

          reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;

          (x + y) = (x1 + y1) & (y + x) = (y1 + x1) by A8;

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

        end;

        hereby

          let x,y,z be Element of W;

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

          (x + (y + z)) = (Av . (x1,(y + z))) by A8;

          then

           A10: (x + (y + z)) = (x1 + (y1 + z1)) by A8;

          ((x + y) + z) = (Av . ((x + y),z1)) by A8;

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

          hence ((x + y) + z) = (x + (y + z)) by A10, RLVECT_1:def 3;

        end;

        hereby

          let x be Element of W;

          reconsider y = x as Element of V by A1, TARSKI:def 3;

          (x + ( 0. W)) = (y + ( 0. V)) by A5, A8;

          hence (x + ( 0. W)) = x;

        end;

        thus W is right_complementable

        proof

          let x be Element of W;

          reconsider x1 = x as Element of V by A1, TARSKI:def 3;

          consider v be Element of V such that

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

          v = ( - x1) by A11, VECTSP_1: 16;

          then

          reconsider y = v as Element of W by A1, A6;

          take y;

          thus thesis by A5, A8, A11;

        end;

        hereby

          let a,b,x be Element of W;

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

          (a * (b * x)) = (MV . (a,(b * x))) by A7;

          then

           A12: (a * (b * x)) = (a1 * (b1 * y)) by A7;

          (a * b) = (a1 * b1) by A7;

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

          hence ((a * b) * x) = (a * (b * x)) by A12, GROUP_1:def 3;

        end;

        hereby

          let x be Element of W;

          reconsider y = x as Element of V by A1, TARSKI:def 3;

          (x * ( 1. W)) = (y * ( 1. V)) & (( 1. W) * x) = (( 1. V) * y) by A4, A7;

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

        end;

        hereby

          let a,x,y be Element of W;

          reconsider x1 = x, y1 = y, a1 = a as Element of V by A1, TARSKI:def 3;

          ((x + y) * a) = (MV . ((x + y),a)) by A7;

          then ((x + y) * a) = ((x1 + y1) * a1) by A8;

          then ((x + y) * a) = ((x1 * a1) + (y1 * a1)) by VECTSP_1:def 7;

          then ((x + y) * a) = (Av . ((MV . (x1,a1)),(y * a))) by A7;

          then

           A13: ((x + y) * a) = (Av . ((x * a),(y * a))) by A7;

          (a * (x + y)) = (MV . (a,(x + y))) by A7;

          then (a * (x + y)) = (a1 * (x1 + y1)) by A8;

          then (a * (x + y)) = ((a1 * x1) + (a1 * y1)) by VECTSP_1:def 7;

          then (a * (x + y)) = (Av . ((MV . (a,x1)),(a * y))) by A7;

          then (a * (x + y)) = (Av . ((a * x),(a * y))) by A7;

          hence (a * (x + y)) = ((a * x) + (a * y)) & ((x + y) * a) = ((x * a) + (y * a)) by A8, A13;

        end;

      end;

      ( 0. W) = ( 0. V) & ( 1. W) = ( 1. V) by A4, A5;

      hence thesis by A1, A2, A3, A9, Def3;

    end;

    registration

      let V be Ring;

      cluster strict for Subring of V;

      existence

      proof

        set V1 = ( [#] V);

        the addF of V = (the addF of V || V1) & the multF of V = (the multF of V || V1) by RELSET_1: 19;

        then doubleLoopStr (# the carrier of V, the addF of V, the multF of V, ( 1. V), ( 0. V) #) is Subring of V by Th1;

        hence thesis;

      end;

    end

    definition

      let V be non empty multLoopStr_0;

      let V1 be Subset of V;

      :: C0SP1:def4

      attr V1 is multiplicatively-closed means ( 1. V) in V1 & for v,u be Element of V st v in V1 & u in V1 holds (v * u) in V1;

    end

    definition

      let V be non empty addLoopStr, V1 be Subset of V;

      :: C0SP1:def5

      func Add_ (V1,V) -> BinOp of V1 equals

      : Def5: (the addF of V || V1);

      correctness

      proof

        

         A2: ( dom the addF of V) = [:the carrier of V, the carrier of V:] by FUNCT_2:def 1;

        

         A3: for z be object st z in [:V1, V1:] holds ((the addF of V || V1) . z) in V1

        proof

          let z be object;

          assume

           A4: z in [:V1, V1:];

          then

          consider r,x be object such that

           A5: r in V1 & x in V1 and

           A6: z = [r, x] by ZFMISC_1:def 2;

          reconsider y = x, r1 = r as Element of V by A5;

           [r, x] in ( dom (the addF of V || V1)) by A2, A4, A6, RELAT_1: 62, ZFMISC_1: 96;

          then ((the addF of V || V1) . z) = (r1 + y) by A6, FUNCT_1: 47;

          hence thesis by A1, A5, IDEAL_1:def 1;

        end;

        ( dom (the addF of V || V1)) = [:V1, V1:] by A2, RELAT_1: 62, ZFMISC_1: 96;

        hence thesis by A3, FUNCT_2: 3;

      end;

    end

    definition

      let V be non empty multLoopStr_0, V1 be Subset of V;

      :: C0SP1:def6

      func mult_ (V1,V) -> BinOp of V1 equals

      : Def6: (the multF of V || V1);

      correctness

      proof

        

         A2: ( dom the multF of V) = [:the carrier of V, the carrier of V:] by FUNCT_2:def 1;

        

         A3: for z be object st z in [:V1, V1:] holds ((the multF of V || V1) . z) in V1

        proof

          let z be object;

          assume

           A4: z in [:V1, V1:];

          then

          consider r,x be object such that

           A5: r in V1 & x in V1 and

           A6: z = [r, x] by ZFMISC_1:def 2;

          reconsider y = x, r1 = r as Element of V by A5;

           [r, x] in ( dom (the multF of V || V1)) by A2, A4, A6, RELAT_1: 62, ZFMISC_1: 96;

          then ((the multF of V || V1) . z) = (r1 * y) by A6, FUNCT_1: 47;

          hence thesis by A1, A5;

        end;

        ( dom (the multF of V || V1)) = [:V1, V1:] by A2, RELAT_1: 62, ZFMISC_1: 96;

        hence thesis by A3, FUNCT_2: 3;

      end;

    end

    definition

      let V be add-associative right_zeroed right_complementable non empty doubleLoopStr, V1 be Subset of V;

      :: C0SP1:def7

      func Zero_ (V1,V) -> Element of V1 equals

      : Def7: ( 0. V);

      correctness

      proof

        set x = the Element of V1;

        reconsider x1 = x as Element of V by A1, TARSKI:def 3;

        ( - x1) in V1 & (x1 + ( - x1)) = ( 0. V) by A1, RLVECT_1:def 10;

        hence thesis by A1, IDEAL_1:def 1;

      end;

    end

    definition

      let V be non empty multLoopStr_0, V1 be Subset of V;

      :: C0SP1:def8

      func One_ (V1,V) -> Element of V1 equals

      : Def8: ( 1. V);

      correctness by A1;

    end

    theorem :: C0SP1:2

    V1 is additively-closed multiplicatively-closed non empty implies doubleLoopStr (# V1, ( Add_ (V1,V)), ( mult_ (V1,V)), ( One_ (V1,V)), ( Zero_ (V1,V)) #) is Ring

    proof

      assume

       A1: V1 is additively-closed multiplicatively-closed non empty;

      then

       A2: ( One_ (V1,V)) = ( 1_ V) & ( mult_ (V1,V)) = (the multF of V || V1) by Def6, Def8;

      ( Zero_ (V1,V)) = ( 0. V) & ( Add_ (V1,V)) = (the addF of V || V1) by A1, Def5, Def7;

      hence thesis by A1, A2, Th1;

    end;

    begin

    reserve V for Algebra;

    reserve V1 for Subset of V;

    reserve MR for Function of [: REAL , X:], X;

    reserve a for Real;

    definition

      let V be Algebra;

      :: C0SP1:def9

      mode Subalgebra of V -> Algebra means

      : Def9: the carrier of it c= the carrier of V & the addF of it = (the addF of V || the carrier of it ) & the multF of it = (the multF of V || the carrier of it ) & the Mult of it = (the Mult of V | [: REAL , the carrier of it :]) & ( 1. it ) = ( 1. V) & ( 0. it ) = ( 0. V);

      existence

      proof

        take V;

        thus the carrier of V c= the carrier of V & the addF of V = (the addF of V || the carrier of V) & the multF of V = (the multF of V || the carrier of V) & the Mult of V = (the Mult of V | [: REAL , the carrier of V:]) & ( 1. V) = ( 1. V) & ( 0. V) = ( 0. V) by RELSET_1: 19;

      end;

    end

    theorem :: C0SP1:3

    

     Th3: V1 = X & d1 = ( 0. V) & d2 = ( 1. V) & A = (the addF of V || V1) & M = (the multF of V || V1) & MR = (the Mult of V | [: REAL , V1:]) & V1 is having-inverse implies AlgebraStr (# X, M, A, MR, d2, d1 #) is Subalgebra of V

    proof

      assume that

       A1: V1 = X and

       A2: d1 = ( 0. V) and

       A3: d2 = ( 1. V) and

       A4: A = (the addF of V || V1) and

       A5: M = (the multF of V || V1) and

       A6: MR = (the Mult of V | [: REAL , V1:]) and

       A7: for v be Element of V st v in V1 holds ( - v) in V1;

      reconsider W = AlgebraStr (# X, M, A, MR, d2, d1 #) as non empty AlgebraStr;

       A8:

      now

        let x,y be Element of W;

        (x + y) = (the addF of V . [x, y]) by A1, A4, FUNCT_1: 49;

        hence (x + y) = (the addF of V . (x,y));

      end;

       A9:

      now

        let a,x be VECTOR of W;

        (a * x) = (the multF of V . [a, x]) by A1, A5, FUNCT_1: 49;

        hence (a * x) = (the multF of V . (a,x));

      end;

       A10:

      now

        let a;

        let x be VECTOR of W;

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

        (aa * x) = (the Mult of V . [aa, x]) by A1, A6, FUNCT_1: 49;

        hence (a * x) = (the Mult of V . (a,x));

      end;

      

       A11: W is Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative

      proof

        set Mv = the multF of V;

        set Av = the addF of V;

        hereby

          let x,y be VECTOR of W;

          reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;

          (x + y) = (x1 + y1) & (y + x) = (y1 + x1) by A8;

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

        end;

        hereby

          let x,y,z be VECTOR of W;

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

          (x + (y + z)) = (Av . (x1,(y + z))) by A8;

          then

           A12: (x + (y + z)) = (x1 + (y1 + z1)) by A8;

          ((x + y) + z) = (Av . ((x + y),z1)) by A8;

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

          hence ((x + y) + z) = (x + (y + z)) by A12, RLVECT_1:def 3;

        end;

        hereby

          let x be VECTOR of W;

          reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

          

          thus (x + ( 0. W)) = (y + ( 0. V)) by A2, A8

          .= x;

        end;

        thus W is right_complementable

        proof

          let x be Element of W;

          reconsider x1 = x as Element of V by A1, TARSKI:def 3;

          consider v be Element of V such that

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

          v = ( - x1) by A13, VECTSP_1: 16;

          then

          reconsider y = v as Element of W by A1, A7;

          take y;

          thus thesis by A2, A8, A13;

        end;

        hereby

          let v,w be Element of W;

          reconsider v1 = v, w1 = w as Element of V by A1, TARSKI:def 3;

          (v * w) = (v1 * w1) & (w * v) = (w1 * v1) by A9;

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

        end;

        hereby

          let a,b,x be Element of W;

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

          (a * (b * x)) = (Mv . (a,(b * x))) by A9;

          then

           A14: (a * (b * x)) = (a1 * (b1 * y)) by A9;

          (a * b) = (a1 * b1) by A9;

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

          hence ((a * b) * x) = (a * (b * x)) by A14, GROUP_1:def 3;

        end;

        hereby

          let v be Element of W;

          reconsider v1 = v as Element of V by A1, TARSKI:def 3;

          (v * ( 1. W)) = (v1 * ( 1. V)) by A3, A9;

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

        end;

        hereby

          let x,y,z be Element of W;

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

          (y + z) = (y1 + z1) by A8;

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

          then

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

          (x * y) = (x1 * y1) & (x * z) = (x1 * z1) by A9;

          hence (x * (y + z)) = ((x * y) + (x * z)) by A8, A15;

        end;

        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, TARSKI:def 3;

          reconsider aa = a as Real;

          

           A16: (aa * x) = (aa * x1) by A10;

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

          then (aa * (x + y)) = (aa * (x1 + y1)) by A10;

          then

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

          (aa * y) = (aa * y1) by A10;

          hence (a * (x + y)) = ((a * x) + (a * y)) by A8, A16, A17;

        end;

        thus W is scalar-distributive

        proof

          let a,b be Real;

          reconsider aa = a, bb = b as Real;

          let x be Element of W;

          reconsider x1 = x as Element of V by A1, TARSKI:def 3;

          

           A18: (aa * x) = (aa * x1) by A10;

          

           A19: (bb * x) = (bb * x1) by A10;

          ((aa + bb) * x) = ((a + b) * x1) by A10;

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

          hence ((a + b) * x) = ((a * x) + (b * x)) by A8, A18, A19;

        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, TARSKI:def 3;

          reconsider aa = a, bb = b as Real;

          

           A20: (bb * x) = (bb * x1) by A10;

          ((aa * bb) * x) = ((a * b) * x1) by A10;

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

          hence ((a * b) * x) = (a * (b * x)) by A10, A20;

        end;

        thus W is vector-associative

        proof

          let x,y be Element of W;

          reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;

          let a be Real;

          

           A21: (a * x) = (a * x1) by A10;

          (x * y) = (x1 * y1) by A9;

          then (a * (x * y)) = (a * (x1 * y1)) by A10;

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

          hence (a * (x * y)) = ((a * x) * y) by A9, A21;

        end;

      end;

      ( 0. W) = ( 0. V) & ( 1. W) = ( 1. V) by A2, A3;

      hence thesis by A1, A4, A5, A6, A11, Def9;

    end;

    registration

      let V be Algebra;

      cluster strict for Subalgebra of V;

      existence

      proof

        set V1 = ( [#] V);

        

         A1: the Mult of V = (the Mult of V | [: REAL , V1:]) by RELSET_1: 19;

        the addF of V = (the addF of V || V1) & the multF of V = (the multF of V || V1) by RELSET_1: 19;

        then AlgebraStr (# the carrier of V, the multF of V, the addF of V, the Mult of V, ( 1. V), ( 0. V) #) is Subalgebra of V by A1, Th3;

        hence thesis;

      end;

    end

    definition

      let V be Algebra, V1 be Subset of V;

      :: C0SP1:def10

      attr V1 is additively-linearly-closed means V1 is add-closed having-inverse & for a be Real, v be Element of V st v in V1 holds (a * v) in V1;

    end

    registration

      let V be Algebra;

      cluster additively-linearly-closed -> additively-closed for Subset of V;

      coherence ;

    end

    definition

      let V be Algebra, V1 be Subset of V;

      :: C0SP1:def11

      func Mult_ (V1,V) -> Function of [: REAL , V1:], V1 equals

      : Def11: (the Mult of V | [: REAL , V1:]);

      correctness

      proof

        

         A2: [: REAL , V1:] c= [: REAL , the carrier of V:] & ( dom the Mult of V) = [: REAL , the carrier of V:] by FUNCT_2:def 1, ZFMISC_1: 95;

        

         A3: for z be object st z in [: REAL , V1:] holds ((the Mult of V | [: REAL , V1:]) . z) in V1

        proof

          let z be object such that

           A4: z in [: REAL , V1:];

          consider r,x be object such that

           A5: r in REAL and

           A6: x in V1 and

           A7: z = [r, x] by A4, ZFMISC_1:def 2;

          reconsider r as Real by A5;

          reconsider y = x as VECTOR of V by A6;

           [r, x] in ( dom (the Mult of V | [: REAL , V1:])) by A2, A4, A7, RELAT_1: 62;

          then ((the Mult of V | [: REAL , V1:]) . z) = (r * y) by A7, FUNCT_1: 47;

          hence thesis by A1, A6;

        end;

        ( dom (the Mult of V | [: REAL , V1:])) = [: REAL , V1:] by A2, RELAT_1: 62;

        hence thesis by A3, FUNCT_2: 3;

      end;

    end

    definition

      let V be non empty RLSStruct;

      :: C0SP1:def12

      attr V is scalar-mult-cancelable means for a be Real, v be Element of V st (a * v) = ( 0. V) holds a = 0 or v = ( 0. V);

    end

    theorem :: C0SP1:4

    

     Th4: for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative vector-associative non empty AlgebraStr, a be Real holds (a * ( 0. V)) = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative vector-associative non empty AlgebraStr;

      let a be Real;

      ((a * ( 0. V)) + (a * ( 0. V))) = (a * (( 0. V) + ( 0. V))) by RLVECT_1:def 5;

      then ((a * ( 0. V)) + (a * ( 0. V))) = (a * ( 0. V));

      then ((a * ( 0. V)) + (a * ( 0. V))) = ((a * ( 0. V)) + ( 0. V));

      hence thesis by RLVECT_1: 8;

    end;

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

    theorem :: C0SP1:5

    for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative vector-associative non empty AlgebraStr st V is scalar-mult-cancelable holds V is RealLinearSpace

    proof

      let V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative vector-associative non empty AlgebraStr;

      assume

       A1: V is scalar-mult-cancelable;

      for v be VECTOR of V holds (1 * v) = v

      proof

        let v be VECTOR of V;

        ((1 * v) + (1 * ( - v))) = (1 * (v + ( - v))) by RLVECT_1:def 5;

        then ((1 * v) - (1 * v)) = ( 0. V) & ((1 * v) + (1 * ( - v))) = (1 * ( 0. V)) by RLVECT_1: 5;

        then

         A2: ( - (jj * v)) = (jj * ( - v)) by Th4, RLVECT_1: 8;

        (1 * v) = ((1 * 1) * v)

        .= (1 * (1 * v)) by RLVECT_1:def 7;

        then ((1 * (1 * v)) - (1 * v)) = ( 0. V) by RLVECT_1: 15;

        then (1 * ((1 * v) - v)) = ( 0. V) by A2, RLVECT_1:def 5;

        then ((jj * v) - v) = ( 0. V) by A1;

        hence thesis by RLVECT_1: 21;

      end;

      hence thesis by RLVECT_1:def 8;

    end;

    

     Lm2: for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative vector-associative non empty AlgebraStr st for v be VECTOR of V holds (1 * v) = v holds V is RealLinearSpace by RLVECT_1:def 8;

    theorem :: C0SP1:6

    

     Th6: V1 is additively-linearly-closed multiplicatively-closed non empty implies AlgebraStr (# V1, ( mult_ (V1,V)), ( Add_ (V1,V)), ( Mult_ (V1,V)), ( One_ (V1,V)), ( Zero_ (V1,V)) #) is Subalgebra of V

    proof

      assume

       A1: V1 is additively-linearly-closed multiplicatively-closed non empty;

      then

       A2: ( Mult_ (V1,V)) = (the Mult of V | [: REAL , V1:]) by Def11;

      

       A3: ( One_ (V1,V)) = ( 1_ V) & ( mult_ (V1,V)) = (the multF of V || V1) by A1, Def6, Def8;

      ( Zero_ (V1,V)) = ( 0. V) & ( Add_ (V1,V)) = (the addF of V || V1) by A1, Def5, Def7;

      hence thesis by A1, A3, A2, Th3;

    end;

    registration

      let X be non empty set;

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

      correctness ;

    end

    theorem :: C0SP1:7

    

     Th7: ( RAlgebra X) is RealLinearSpace

    proof

      for v be VECTOR of ( RAlgebra X) holds (1 * v) = v by FUNCSDOM: 12;

      hence thesis by Lm2;

    end;

    theorem :: C0SP1:8

    

     Th8: for V be Algebra, V1 be Subalgebra of V holds (for v1,w1 be Element of V1, v,w be Element of V st v1 = v & w1 = w holds (v1 + w1) = (v + w)) & (for v1,w1 be Element of V1, v,w be Element of V st v1 = v & w1 = w holds (v1 * w1) = (v * w)) & (for v1 be Element of V1, v be Element of V, a be Real st v1 = v holds (a * v1) = (a * v)) & ( 1_ V1) = ( 1_ V) & ( 0. V1) = ( 0. V)

    proof

      let V be Algebra, V1 be Subalgebra of V;

      hereby

        let x1,y1 be Element of V1, x,y be Element of V;

        assume

         A1: x1 = x & y1 = y;

        (x1 + y1) = ((the addF of V || the carrier of V1) . [x1, y1]) by Def9;

        hence (x1 + y1) = (x + y) by A1, FUNCT_1: 49;

      end;

      hereby

        let x1,y1 be Element of V1, x,y be Element of V;

        assume

         A2: x1 = x & y1 = y;

        (x1 * y1) = ((the multF of V || the carrier of V1) . [x1, y1]) by Def9;

        hence (x1 * y1) = (x * y) by A2, FUNCT_1: 49;

      end;

      hereby

        let v1 be Element of V1, v be Element of V, a be Real;

        assume

         A3: v1 = v;

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

        (aa * v1) = ((the Mult of V | [: REAL , the carrier of V1:]) . [aa, v1]) by Def9;

        then (aa * v1) = (aa * v) by A3, FUNCT_1: 49;

        hence (a * v1) = (a * v);

      end;

      thus thesis by Def9;

    end;

    begin

    definition

      let X be non empty set;

      :: C0SP1:def13

      func BoundedFunctions X -> non empty Subset of ( RAlgebra X) equals { f where f be Function of X, REAL : (f | X) is bounded };

      correctness

      proof

        

         A1: { f where f be Function of X, REAL : (f | X) is bounded } is non empty

        proof

          reconsider g = (X --> ( In ( 0 , REAL ))) as Function of X, REAL ;

          (g | X) is bounded;

          then g in { f where f be Function of X, REAL : (f | X) is bounded };

          hence thesis;

        end;

        { f where f be Function of X, REAL : (f | X) is bounded } c= ( Funcs (X, REAL ))

        proof

          let x be object;

          assume x in { f where f be Function of X, REAL : (f | X) is bounded };

          then ex f be Function of X, REAL st x = f & (f | X) is bounded;

          hence thesis by FUNCT_2: 8;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: C0SP1:9

    

     Th9: ( BoundedFunctions X) is additively-linearly-closed multiplicatively-closed

    proof

      set W = ( BoundedFunctions X);

      set V = ( RAlgebra X);

      

       A1: 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 and

         A3: u in W;

        consider u1 be Function of X, REAL such that

         A4: u1 = u and

         A5: (u1 | X) is bounded by A3;

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

        consider v1 be Function of X, REAL such that

         A6: v1 = v and

         A7: (v1 | X) is bounded by A2;

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

        then

         A8: ((v1 (#) u1) | X) is bounded by A7, A5, RFUNCT_1: 84;

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

        then

         A9: (ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL ) & (( dom v1) /\ ( dom u1)) = (X /\ X) by FUNCT_2:def 1, FUNCT_2:def 2;

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

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

        hence thesis by A8;

      end;

      reconsider g = ( RealFuncUnit X) as Function of X, REAL ;

      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

         A10: v in W and

         A11: u in W;

        consider u1 be Function of X, REAL such that

         A12: u1 = u and

         A13: (u1 | X) is bounded by A11;

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

        consider v1 be Function of X, REAL such that

         A14: v1 = v and

         A15: (v1 | X) is bounded by A10;

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

        then

         A16: ((v1 + u1) | X) is bounded by A15, A13, RFUNCT_1: 83;

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

        then

         A17: (ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL ) & (( dom v1) /\ ( dom u1)) = (X /\ X) by FUNCT_2:def 1, FUNCT_2:def 2;

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

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

        hence thesis by A16;

      end;

      then

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

      

       A19: ( RAlgebra X) is RealLinearSpace by Th7;

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

      proof

        let v be Element of V;

        assume v in W;

        then

        consider v1 be Function of X, REAL such that

         A20: v1 = v and

         A21: (v1 | X) is bounded;

        

         A22: (( - v1) | X) is bounded by A21, RFUNCT_1: 82;

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

        

         A23: h = (( - 1) * v) by A19, RLVECT_1: 16;

         A24:

        now

          let x be object;

          assume x in ( dom h);

          then

          reconsider y = x as Element of X;

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

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

        end;

        (ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL ) & ( dom v1) = X by FUNCT_2:def 1, FUNCT_2:def 2;

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

        hence thesis by A22;

      end;

      then

       A25: 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;

        assume u in W;

        then

        consider u1 be Function of X, REAL such that

         A26: u1 = u and

         A27: (u1 | X) is bounded;

        

         A28: ((a (#) u1) | X) is bounded by A27, RFUNCT_1: 80;

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

        

         A29: (ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL ) & ( dom u1) = X by FUNCT_2:def 1, FUNCT_2:def 2;

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

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

        hence thesis by A28;

      end;

      hence ( BoundedFunctions X) is additively-linearly-closed by A18, A25;

      (g | X) is bounded;

      then ( 1. V) in W;

      hence thesis by A1;

    end;

    registration

      let X;

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

      coherence by Th9;

    end

    definition

      let X be non empty set;

      :: C0SP1:def14

      func R_Algebra_of_BoundedFunctions X -> Algebra equals AlgebraStr (# ( BoundedFunctions X), ( mult_ (( BoundedFunctions X),( RAlgebra X))), ( Add_ (( BoundedFunctions X),( RAlgebra X))), ( Mult_ (( BoundedFunctions X),( RAlgebra X))), ( One_ (( BoundedFunctions X),( RAlgebra X))), ( Zero_ (( BoundedFunctions X),( RAlgebra X))) #);

      coherence by Th6;

    end

    theorem :: C0SP1:10

    ( R_Algebra_of_BoundedFunctions X) is Subalgebra of ( RAlgebra X) by Th6;

    theorem :: C0SP1:11

    ( R_Algebra_of_BoundedFunctions X) is RealLinearSpace

    proof

      now

        let v be VECTOR of ( R_Algebra_of_BoundedFunctions X);

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

        ( R_Algebra_of_BoundedFunctions X) is Subalgebra of ( RAlgebra X) by Th6;

        then (jj * v) = (jj * v1) by Th8;

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

      end;

      hence thesis by Lm2;

    end;

    reserve F,G,H for VECTOR of ( R_Algebra_of_BoundedFunctions X);

    reserve f,g,h for Function of X, REAL ;

    theorem :: C0SP1:12

    

     Th12: 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

      assume

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

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

      

       A2: ( R_Algebra_of_BoundedFunctions X) is Subalgebra of ( RAlgebra X) by Th6;

      hereby

        assume

         A3: H = (F + G);

        let x be Element of X;

        h1 = (f1 + g1) by A2, A3, Th8;

        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 thesis by A2, Th8;

    end;

    theorem :: C0SP1:13

    

     Th13: f = F & g = G implies (G = (a * F) iff for x be Element of X holds (g . x) = (a * (f . x)))

    proof

      assume

       A1: f = F & g = G;

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

      

       A2: ( R_Algebra_of_BoundedFunctions X) is Subalgebra of ( RAlgebra X) by Th6;

      hereby

        assume

         A3: G = (a * F);

        let x be Element of X;

        g1 = (a * f1) by A2, A3, Th8;

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

      end;

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

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

      hence thesis by A2, Th8;

    end;

    theorem :: C0SP1:14

    

     Th14: 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

      assume

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

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

      

       A2: ( R_Algebra_of_BoundedFunctions X) is Subalgebra of ( RAlgebra X) by Th6;

      hereby

        assume

         A3: H = (F * G);

        let x be Element of X;

        h1 = (f1 * g1) by A2, A3, Th8;

        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 thesis by A2, Th8;

    end;

    theorem :: C0SP1:15

    

     Th15: ( 0. ( R_Algebra_of_BoundedFunctions X)) = (X --> 0 )

    proof

      ( R_Algebra_of_BoundedFunctions X) is Subalgebra of ( RAlgebra X) & ( 0. ( RAlgebra X)) = (X --> 0 ) by Th6;

      hence thesis by Th8;

    end;

    theorem :: C0SP1:16

    

     Th16: ( 1_ ( R_Algebra_of_BoundedFunctions X)) = (X --> 1)

    proof

      ( R_Algebra_of_BoundedFunctions X) is Subalgebra of ( RAlgebra X) & ( 1_ ( RAlgebra X)) = (X --> 1) by Th6;

      hence thesis by Th8;

    end;

    definition

      let X be non empty set, F be object;

      :: C0SP1:def15

      func modetrans (F,X) -> Function of X, REAL means

      : Def15: it = F & (it | X) is bounded;

      correctness by A1;

    end

    definition

      let X be non empty set, f be Function of X, REAL ;

      :: C0SP1:def16

      func PreNorms f -> non empty Subset of REAL equals the set of all |.(f . x).| where x be Element of X;

      coherence

      proof

        set z = the Element of X;

         A1:

        now

          let z be object;

          now

            assume z in the set of all |.(f . x).| where x be Element of X;

            then ex x be Element of X st z = |.(f . x).|;

            hence z in REAL by XREAL_0:def 1;

          end;

          hence z in the set of all |.(f . x).| where x be Element of X implies z in REAL ;

        end;

         |.(f . z).| in the set of all |.(f . x).| where x be Element of X;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: C0SP1:17

    

     Th17: (f | X) is bounded implies ( PreNorms f) is bounded_above

    proof

      assume (f | X) is bounded;

      then

      consider K be Real such that

       A1: for x be object st x in (X /\ ( dom f)) holds |.(f . x).| <= K by RFUNCT_1: 73;

      

       A2: (X /\ ( dom f)) = (X /\ X) by FUNCT_2:def 1;

      take K;

      let r be ExtReal;

      assume r in ( PreNorms f);

      then ex t be Element of X st r = |.(f . t).|;

      hence r <= K by A1, A2;

    end;

    theorem :: C0SP1:18

    (f | X) is bounded iff ( PreNorms f) is bounded_above

    proof

      now

        reconsider K = ( upper_bound ( PreNorms f)) as Real;

        assume

         A1: ( PreNorms f) is bounded_above;

        take K;

        now

          let t be object;

          assume t in (X /\ ( dom f));

          then |.(f . t).| in ( PreNorms f);

          hence |.(f . t).| <= K by A1, SEQ_4:def 1;

        end;

        hence (f | X) is bounded by RFUNCT_1: 73;

      end;

      hence thesis by Th17;

    end;

    definition

      let X be non empty set;

      :: C0SP1:def17

      func BoundedFunctionsNorm X -> Function of ( BoundedFunctions X), REAL means

      : Def17: for x be object st x in ( BoundedFunctions X) holds (it . x) = ( upper_bound ( PreNorms ( modetrans (x,X))));

      existence

      proof

        deffunc F( object) = ( upper_bound ( PreNorms ( modetrans ($1,X))));

        

         A1: for z be object st z in ( BoundedFunctions X) holds F(z) in REAL by XREAL_0:def 1;

        ex f be Function of ( BoundedFunctions X), REAL st for x be object st x in ( BoundedFunctions X) holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let NORM1,NORM2 be Function of ( BoundedFunctions X), REAL such that

         A2: for x be object st x in ( BoundedFunctions X) holds (NORM1 . x) = ( upper_bound ( PreNorms ( modetrans (x,X)))) and

         A3: for x be object st x in ( BoundedFunctions X) holds (NORM2 . x) = ( upper_bound ( PreNorms ( modetrans (x,X))));

        

         A4: for z be object st z in ( BoundedFunctions X) holds (NORM1 . z) = (NORM2 . z)

        proof

          let z be object such that

           A5: z in ( BoundedFunctions X);

          (NORM1 . z) = ( upper_bound ( PreNorms ( modetrans (z,X)))) by A2, A5;

          hence thesis by A3, A5;

        end;

        ( dom NORM1) = ( BoundedFunctions X) & ( dom NORM2) = ( BoundedFunctions X) by FUNCT_2:def 1;

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    theorem :: C0SP1:19

    

     Th19: (f | X) is bounded implies ( modetrans (f,X)) = f

    proof

      assume (f | X) is bounded;

      then f in ( BoundedFunctions X);

      hence thesis by Def15;

    end;

    theorem :: C0SP1:20

    

     Th20: (f | X) is bounded implies (( BoundedFunctionsNorm X) . f) = ( upper_bound ( PreNorms f))

    proof

      reconsider f9 = f as set;

      assume

       A1: (f | X) is bounded;

      then f in ( BoundedFunctions X);

      then (( BoundedFunctionsNorm X) . f) = ( upper_bound ( PreNorms ( modetrans (f9,X)))) by Def17;

      hence thesis by A1, Th19;

    end;

    definition

      let X be non empty set;

      :: C0SP1:def18

      func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals Normed_AlgebraStr (# ( BoundedFunctions X), ( mult_ (( BoundedFunctions X),( RAlgebra X))), ( Add_ (( BoundedFunctions X),( RAlgebra X))), ( Mult_ (( BoundedFunctions X),( RAlgebra X))), ( One_ (( BoundedFunctions X),( RAlgebra X))), ( Zero_ (( BoundedFunctions X),( RAlgebra X))), ( BoundedFunctionsNorm X) #);

      correctness ;

    end

    registration

      let X be non empty set;

      cluster ( R_Normed_Algebra_of_BoundedFunctions X) -> non empty;

      correctness ;

    end

     Lm3:

    now

      let X be non empty set;

      set F = ( R_Normed_Algebra_of_BoundedFunctions X);

      let x,e be Element of F;

      set X1 = ( BoundedFunctions X);

      reconsider f = x as Element of X1;

      assume

       A1: e = ( One_ (( BoundedFunctions X),( RAlgebra X)));

      then (x * e) = (( mult_ (X1,( RAlgebra X))) . (f,( 1_ ( RAlgebra X)))) by Def8;

      then

       A2: (x * e) = ((the multF of ( RAlgebra X) || X1) . (f,( 1_ ( RAlgebra X)))) by Def6;

      (e * x) = (( mult_ (X1,( RAlgebra X))) . (( 1_ ( RAlgebra X)),f)) by A1, Def8;

      then

       A3: (e * x) = ((the multF of ( RAlgebra X) || X1) . (( 1_ ( RAlgebra X)),f)) by Def6;

      

       A4: ( 1_ ( RAlgebra X)) = ( 1_ ( R_Algebra_of_BoundedFunctions X)) by Th16;

      then [f, ( 1_ ( RAlgebra X))] in [:X1, X1:] by ZFMISC_1: 87;

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

      hence (x * e) = x;

       [( 1_ ( RAlgebra X)), f] in [:X1, X1:] by A4, ZFMISC_1: 87;

      then (e * x) = (( 1_ ( RAlgebra X)) * f) by A3, FUNCT_1: 49;

      hence (e * x) = x;

    end;

    registration

      let X be non empty set;

      cluster ( R_Normed_Algebra_of_BoundedFunctions X) -> unital;

      correctness

      proof

        reconsider e = ( One_ (( BoundedFunctions X),( RAlgebra X))) as Element of ( R_Normed_Algebra_of_BoundedFunctions X);

        take e;

        thus thesis by Lm3;

      end;

    end

    theorem :: C0SP1:21

    

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

      end;

      

       A3: 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 thesis by A1;

      end;

      

       A4: 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

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

        reconsider y = v as Element of W by A1;

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

        hence thesis;

      end;

      

       A6: 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 thesis by A1;

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

      end;

      

       A8: 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 thesis by A1;

      end;

      

       A9: 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 thesis by A1;

      end;

      

       A10: 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;

      

       A11: 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;

        thus thesis;

      end;

      

       A12: 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 thesis by A1;

      end;

      

       A13: W is vector-associative

      proof

        let x,y be Element of W;

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

        let a be Real;

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

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

      end;

      hence thesis by A9, A8, A4, A7, A6, A2, A3, A10, A11, A12, A13, 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;

    reserve F,G,H for Point of ( R_Normed_Algebra_of_BoundedFunctions X);

    theorem :: C0SP1:22

    

     Th22: ( R_Normed_Algebra_of_BoundedFunctions X) is Algebra

    proof

      ( 1. ( R_Normed_Algebra_of_BoundedFunctions X)) = ( 1_ ( R_Algebra_of_BoundedFunctions X));

      hence thesis by Th21;

    end;

    theorem :: C0SP1:23

    

     Th23: (( Mult_ (( BoundedFunctions X),( RAlgebra X))) . (1,F)) = F

    proof

      set X1 = ( BoundedFunctions X);

      reconsider f1 = F as Element of X1;

      

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

      

      thus (( Mult_ (( BoundedFunctions X),( RAlgebra X))) . (1,F)) = ((the Mult of ( RAlgebra X) | [: REAL , X1:]) . (1,f1)) by Def11

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

      .= F by FUNCSDOM: 12;

    end;

    theorem :: C0SP1:24

    

     Th24: ( R_Normed_Algebra_of_BoundedFunctions X) is RealLinearSpace

    proof

      (for v be VECTOR of ( R_Normed_Algebra_of_BoundedFunctions X) holds (1 * v) = v) & ( R_Normed_Algebra_of_BoundedFunctions X) is Algebra by Th22, Th23;

      hence thesis by Lm2;

    end;

    theorem :: C0SP1:25

    

     Th25: (X --> 0 ) = ( 0. ( R_Normed_Algebra_of_BoundedFunctions X))

    proof

      (X --> 0 ) = ( 0. ( R_Algebra_of_BoundedFunctions X)) by Th15;

      hence thesis;

    end;

    theorem :: C0SP1:26

    

     Th26: f = F & (f | X) is bounded implies |.(f . x).| <= ||.F.||

    proof

      assume that

       A1: f = F and

       A2: (f | X) is bounded;

      

       A3: |.(f . x).| in ( PreNorms f);

      ( PreNorms f) is non empty bounded_above by A2, Th17;

      then |.(f . x).| <= ( upper_bound ( PreNorms f)) by A3, SEQ_4:def 1;

      hence thesis by A1, A2, Th20;

    end;

    theorem :: C0SP1:27

     0 <= ||.F.||

    proof

      F in ( BoundedFunctions X);

      then

      consider g be Function of X, REAL such that

       A1: F = g and

       A2: (g | X) is bounded;

      

       A3: ( PreNorms g) is non empty bounded_above by A2, Th17;

      consider r0 be object such that

       A4: r0 in ( PreNorms g) by XBOOLE_0:def 1;

      reconsider r0 as Real by A4;

      now

        let r be Real;

        assume r in ( PreNorms g);

        then ex t be Element of X st r = |.(g . t).|;

        hence 0 <= r by COMPLEX1: 46;

      end;

      then 0 <= r0 by A4;

      then 0 <= ( upper_bound ( PreNorms g)) by A3, A4, SEQ_4:def 1;

      hence thesis by A1, A2, Th20;

    end;

    theorem :: C0SP1:28

    

     Th28: F = ( 0. ( R_Normed_Algebra_of_BoundedFunctions X)) implies 0 = ||.F.||

    proof

      set z = (X --> ( In ( 0 , REAL )));

      reconsider z as Function of X, REAL ;

      F in ( BoundedFunctions X);

      then

      consider g be Function of X, REAL such that

       A1: g = F and

       A2: (g | X) is bounded;

      

       A3: ( PreNorms g) is non empty bounded_above by A2, Th17;

      consider r0 be object such that

       A4: r0 in ( PreNorms g) by XBOOLE_0:def 1;

      reconsider r0 as Real by A4;

      

       A5: (for s be Real st s in ( PreNorms g) holds s <= 0 ) implies ( upper_bound ( PreNorms g)) <= 0 by SEQ_4: 45;

      assume

       A6: F = ( 0. ( R_Normed_Algebra_of_BoundedFunctions X));

       A7:

      now

        let r be Real;

        assume r in ( PreNorms g);

        then

        consider t be Element of X such that

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

        z = g by A6, A1, Th25;

        then |.(g . t).| = |. 0 .|;

        hence 0 <= r & r <= 0 by A8, ABSVALUE: 2;

      end;

      then 0 <= r0 by A4;

      then ( upper_bound ( PreNorms g)) = 0 by A7, A3, A4, A5, SEQ_4:def 1;

      hence thesis by A1, A2, Th20;

    end;

    theorem :: C0SP1:29

    

     Th29: 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

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

      

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

      assume f = F & g = G & h = H;

      hence thesis by A1, Th12;

    end;

    theorem :: C0SP1:30

    

     Th30: f = F & g = G implies (G = (a * F) iff for x be Element of X holds (g . x) = (a * (f . x)))

    proof

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

      

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

      assume f = F & g = G;

      hence thesis by A1, Th13;

    end;

    theorem :: C0SP1:31

    

     Th31: 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

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

      

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

      assume f = F & g = G & h = H;

      hence thesis by A1, Th14;

    end;

    theorem :: C0SP1:32

    

     Th32: ( ||.F.|| = 0 iff F = ( 0. ( R_Normed_Algebra_of_BoundedFunctions X))) & ||.(a * F).|| = ( |.a.| * ||.F.||) & ||.(F + G).|| <= ( ||.F.|| + ||.G.||)

    proof

       A1:

      now

        set z = (X --> ( In ( 0 , REAL )));

        reconsider z as Function of X, REAL ;

        F in ( BoundedFunctions X);

        then

        consider g be Function of X, REAL such that

         A2: F = g and

         A3: (g | X) is bounded;

        

         A4: ( PreNorms g) is non empty bounded_above by A3, Th17;

        consider r0 be object such that

         A5: r0 in ( PreNorms g) by XBOOLE_0:def 1;

        reconsider r0 as Real by A5;

        

         A6: (for s be Real st s in ( PreNorms g) holds s <= 0 ) implies ( upper_bound ( PreNorms g)) <= 0 by SEQ_4: 45;

        assume F = ( 0. ( R_Normed_Algebra_of_BoundedFunctions X));

        then

         A7: z = g by A2, Th25;

         A8:

        now

          let r be Real;

          assume r in ( PreNorms g);

          then

          consider t be Element of X such that

           A9: r = |.(g . t).|;

           |.(g . t).| = |. 0 .| by A7

          .= 0 by ABSVALUE: 2;

          hence 0 <= r & r <= 0 by A9;

        end;

        then 0 <= r0 by A5;

        then ( upper_bound ( PreNorms g)) = 0 by A8, A4, A5, A6, SEQ_4:def 1;

        hence ||.F.|| = 0 by A2, A3, Th20;

      end;

      

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

      proof

        (F + G) in ( BoundedFunctions X);

        then

        consider h1 be Function of X, REAL such that

         A11: h1 = (F + G) and

         A12: (h1 | X) is bounded;

        G in ( BoundedFunctions X);

        then

        consider g1 be Function of X, REAL such that

         A13: g1 = G and

         A14: (g1 | X) is bounded;

        F in ( BoundedFunctions X);

        then

        consider f1 be Function of X, REAL such that

         A15: f1 = F and

         A16: (f1 | X) is bounded;

         A17:

        now

          let t be Element of X;

           |.(f1 . t).| <= ||.F.|| & |.(g1 . t).| <= ||.G.|| by A15, A16, A13, A14, Th26;

          then

           A18: ( |.(f1 . t).| + |.(g1 . t).|) <= ( ||.F.|| + ||.G.||) by XREAL_1: 7;

           |.(h1 . t).| = |.((f1 . t) + (g1 . t)).| & |.((f1 . t) + (g1 . t)).| <= ( |.(f1 . t).| + |.(g1 . t).|) by A15, A13, A11, Th29, COMPLEX1: 56;

          hence |.(h1 . t).| <= ( ||.F.|| + ||.G.||) by A18, XXREAL_0: 2;

        end;

         A19:

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then ex t be Element of X st r = |.(h1 . t).|;

          hence r <= ( ||.F.|| + ||.G.||) by A17;

        end;

        (for s be Real st s in ( PreNorms h1) holds s <= ( ||.F.|| + ||.G.||)) implies ( upper_bound ( PreNorms h1)) <= ( ||.F.|| + ||.G.||) by SEQ_4: 45;

        hence thesis by A11, A12, A19, Th20;

      end;

      

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

      proof

        F in ( BoundedFunctions X);

        then

        consider f1 be Function of X, REAL such that

         A21: f1 = F and

         A22: (f1 | X) is bounded;

        (a * F) in ( BoundedFunctions X);

        then

        consider h1 be Function of X, REAL such that

         A23: h1 = (a * F) and

         A24: (h1 | X) is bounded;

         A25:

        now

          let t be Element of X;

           |.(h1 . t).| = |.(a * (f1 . t)).| by A21, A23, Th30;

          then

           A26: |.(h1 . t).| = ( |.a.| * |.(f1 . t).|) by COMPLEX1: 65;

           0 <= |.a.| by COMPLEX1: 46;

          hence |.(h1 . t).| <= ( |.a.| * ||.F.||) by A21, A22, A26, Th26, XREAL_1: 64;

        end;

         A27:

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then ex t be Element of X st r = |.(h1 . t).|;

          hence r <= ( |.a.| * ||.F.||) by A25;

        end;

        (for s be Real st s in ( PreNorms h1) holds s <= ( |.a.| * ||.F.||)) implies ( upper_bound ( PreNorms h1)) <= ( |.a.| * ||.F.||) by SEQ_4: 45;

        then

         A28: ||.(a * F).|| <= ( |.a.| * ||.F.||) by A23, A24, A27, Th20;

        per cases ;

          suppose

           A29: a <> 0 ;

           A30:

          now

            let t be Element of X;

             |.(a " ).| = |.(1 / a).|;

            then

             A31: |.(a " ).| = (1 / |.a.|) by ABSVALUE: 7;

            (h1 . t) = (a * (f1 . t)) by A21, A23, Th30;

            then ((a " ) * (h1 . t)) = (((a " ) * a) * (f1 . t));

            then

             A32: ((a " ) * (h1 . t)) = (1 * (f1 . t)) by A29, XCMPLX_0:def 7;

             |.((a " ) * (h1 . t)).| = ( |.(a " ).| * |.(h1 . t).|) & 0 <= |.(a " ).| by COMPLEX1: 46, COMPLEX1: 65;

            hence |.(f1 . t).| <= (( |.a.| " ) * ||.(a * F).||) by A23, A24, A32, A31, Th26, XREAL_1: 64;

          end;

           A33:

          now

            let r be Real;

            assume r in ( PreNorms f1);

            then ex t be Element of X st r = |.(f1 . t).|;

            hence r <= (( |.a.| " ) * ||.(a * F).||) by A30;

          end;

          

           A34: 0 <= |.a.| by COMPLEX1: 46;

          (for s be Real st s in ( PreNorms f1) holds s <= (( |.a.| " ) * ||.(a * F).||)) implies ( upper_bound ( PreNorms f1)) <= (( |.a.| " ) * ||.(a * F).||) by SEQ_4: 45;

          then ||.F.|| <= (( |.a.| " ) * ||.(a * F).||) by A21, A22, A33, Th20;

          then ( |.a.| * ||.F.||) <= ( |.a.| * (( |.a.| " ) * ||.(a * F).||)) by A34, XREAL_1: 64;

          then

           A35: ( |.a.| * ||.F.||) <= (( |.a.| * ( |.a.| " )) * ||.(a * F).||);

           |.a.| <> 0 by A29, COMPLEX1: 47;

          then ( |.a.| * ||.F.||) <= (1 * ||.(a * F).||) by A35, XCMPLX_0:def 7;

          hence thesis by A28, XXREAL_0: 1;

        end;

          suppose

           A36: a = 0 ;

          reconsider fz = F as VECTOR of ( R_Algebra_of_BoundedFunctions X);

          (a * fz) = ((a + a) * fz) by A36

          .= ((a * fz) + (a * fz)) by RLVECT_1:def 6;

          then ( 0. ( R_Algebra_of_BoundedFunctions X)) = (( - (a * fz)) + ((a * fz) + (a * fz))) by VECTSP_1: 16;

          then ( 0. ( R_Algebra_of_BoundedFunctions X)) = ((( - (a * fz)) + (a * fz)) + (a * fz)) by RLVECT_1:def 3;

          then ( 0. ( R_Algebra_of_BoundedFunctions X)) = (( 0. ( R_Algebra_of_BoundedFunctions X)) + (a * fz)) by VECTSP_1: 16;

          then

           A37: (a * F) = ( 0. ( R_Normed_Algebra_of_BoundedFunctions X));

          ( |.a.| * ||.F.||) = ( 0 * ||.F.||) by A36, ABSVALUE: 2;

          hence thesis by A37, Th28;

        end;

      end;

      now

        set z = (X --> ( In ( 0 , REAL )));

        reconsider z as Function of X, REAL ;

        F in ( BoundedFunctions X);

        then

        consider g be Function of X, REAL such that

         A38: F = g and

         A39: (g | X) is bounded;

        assume

         A40: ||.F.|| = 0 ;

        now

          let t be Element of X;

           |.(g . t).| <= ||.F.|| by A38, A39, Th26;

          then |.(g . t).| = 0 by A40, COMPLEX1: 46;

          

          hence (g . t) = 0 by ABSVALUE: 2

          .= (z . t);

        end;

        then g = z by FUNCT_2: 63;

        hence F = ( 0. ( R_Normed_Algebra_of_BoundedFunctions X)) by A38, Th25;

      end;

      hence thesis by A1, A20, A10;

    end;

    theorem :: C0SP1:33

    

     Th33: ( R_Normed_Algebra_of_BoundedFunctions X) is reflexive discerning RealNormSpace-like

    proof

      thus ||.( 0. ( R_Normed_Algebra_of_BoundedFunctions X)).|| = 0 by Th32;

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

      hence thesis by NORMSP_1:def 1;

    end;

    registration

      let X be non empty set;

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

      coherence by Th24, Th33;

    end

    theorem :: C0SP1:34

    

     Th34: 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

      assume

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

       A2:

      now

        assume

         A3: 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 A3;

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

        end;

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

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

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

        hence (F - G) = H;

      end;

      now

        assume H = (F - G);

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

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

        then

         A4: (H + G) = F;

        now

          let x be Element of X;

          (f . x) = ((h . x) + (g . x)) by A1, A4, Th29;

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

        end;

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

      end;

      hence thesis by A2;

    end;

    theorem :: C0SP1:35

    

     Th35: for X be non empty set holds for seq be sequence of ( R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds seq is convergent

    proof

      let X be non empty set;

      let vseq be sequence of ( R_Normed_Algebra_of_BoundedFunctions X);

      defpred P[ set, set] means ex xseq be Real_Sequence st (for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X)) . $1)) & xseq is convergent & $2 = ( lim xseq);

      assume

       A1: vseq is Cauchy_sequence_by_Norm;

      

       A2: for x be Element of X holds ex y be Element of REAL st P[x, y]

      proof

        let x be Element of X;

        deffunc F( Nat) = (( modetrans ((vseq . $1),X)) . x);

        consider xseq be Real_Sequence such that

         A3: for n be Element of NAT holds (xseq . n) = F(n) from FUNCT_2:sch 4;

        

         A4: for n be Nat holds (xseq . n) = F(n)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A3;

        end;

        reconsider lx = ( lim xseq) as Element of REAL by XREAL_0:def 1;

        take lx;

        

         A5: for m,k be Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

        proof

          let m,k be Nat;

          ((vseq . m) - (vseq . k)) in ( BoundedFunctions X);

          then

          consider h1 be Function of X, REAL such that

           A6: h1 = ((vseq . m) - (vseq . k)) and

           A7: (h1 | X) is bounded;

          (vseq . m) in ( BoundedFunctions X);

          then ex vseqm be Function of X, REAL st (vseq . m) = vseqm & (vseqm | X) is bounded;

          then

           A8: ( modetrans ((vseq . m),X)) = (vseq . m) by Th19;

          (vseq . k) in ( BoundedFunctions X);

          then ex vseqk be Function of X, REAL st (vseq . k) = vseqk & (vseqk | X) is bounded;

          then

           A9: ( modetrans ((vseq . k),X)) = (vseq . k) by Th19;

          (xseq . m) = (( modetrans ((vseq . m),X)) . x) & (xseq . k) = (( modetrans ((vseq . k),X)) . x) by A4;

          then ((xseq . m) - (xseq . k)) = (h1 . x) by A8, A9, A6, Th34;

          hence thesis by A6, A7, Th26;

        end;

        now

          let e be Real such that

           A10: e > 0 ;

          consider k be Nat such that

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

          take k;

          let n be Nat;

          assume n >= k;

          then

           A12: ||.((vseq . n) - (vseq . k)).|| < e by A11;

           |.((xseq . n) - (xseq . k)).| <= ||.((vseq . n) - (vseq . k)).|| by A5;

          hence |.((xseq . n) - (xseq . k)).| < e by A12, XXREAL_0: 2;

        end;

        then xseq is convergent by SEQ_4: 41;

        hence thesis by A4;

      end;

      consider tseq be Function of X, REAL such that

       A13: for x be Element of X holds P[x, (tseq . x)] from FUNCT_2:sch 3( A2);

      now

        let e1 be Real such that

         A14: e1 > 0 ;

        reconsider e = e1 as Real;

        consider k be Nat such that

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

        take k;

        let m be Nat;

        

         A16: ||.(vseq . m).|| = ( ||.vseq.|| . m) by NORMSP_0:def 4;

        assume m >= k;

        then

         A17: ||.((vseq . m) - (vseq . k)).|| < e by A15;

         |.( ||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ( ||.vseq.|| . k) by NORMSP_0:def 4, NORMSP_1: 9;

        hence |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1 by A17, A16, XXREAL_0: 2;

      end;

      then

       A18: ||.vseq.|| is convergent by SEQ_4: 41;

      now

        let x be object;

        assume

         A19: x in (X /\ ( dom tseq));

        then

        consider xseq be Real_Sequence such that

         A20: for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X)) . x) and

         A21: xseq is convergent & (tseq . x) = ( lim xseq) by A13;

        

         A22: for n be Nat holds (( abs xseq) . n) <= ( ||.vseq.|| . n)

        proof

          let n be Nat;

          

           A23: (xseq . n) = (( modetrans ((vseq . n),X)) . x) by A20;

          (vseq . n) in ( BoundedFunctions X);

          then

           A24: ex h1 be Function of X, REAL st (vseq . n) = h1 & (h1 | X) is bounded;

          then ( modetrans ((vseq . n),X)) = (vseq . n) by Th19;

          then |.(xseq . n).| <= ||.(vseq . n).|| by A19, A24, A23, Th26;

          then (( abs xseq) . n) <= ||.(vseq . n).|| by VALUED_1: 18;

          hence thesis by NORMSP_0:def 4;

        end;

        ( abs xseq) is convergent & |.(tseq . x).| = ( lim ( abs xseq)) by A21, SEQ_4: 14;

        hence |.(tseq . x).| <= ( lim ||.vseq.||) by A18, A22, SEQ_2: 18;

      end;

      then (tseq | X) is bounded by RFUNCT_1: 73;

      then tseq in ( BoundedFunctions X);

      then

      reconsider tv = tseq as Point of ( R_Normed_Algebra_of_BoundedFunctions X);

      

       A25: for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds for x be Element of X holds |.((( modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

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

        take k;

        let n be Nat such that

         A27: n >= k;

        now

          let x be Element of X;

          consider xseq be Real_Sequence such that

           A28: for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X)) . x) and

           A29: xseq is convergent and

           A30: (tseq . x) = ( lim xseq) by A13;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          set fseq = ( seq_const (xseq . n));

          set wseq = (xseq - fseq);

          deffunc F( Nat) = |.((xseq . $1) - (xseq . n)).|;

          consider rseq be Real_Sequence such that

           A31: for m be Nat holds (rseq . m) = F(m) from SEQ_1:sch 1;

          

           A32: for m,k be Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

          proof

            let m,k be Nat;

            ((vseq . m) - (vseq . k)) in ( BoundedFunctions X);

            then

            consider h1 be Function of X, REAL such that

             A33: h1 = ((vseq . m) - (vseq . k)) and

             A34: (h1 | X) is bounded;

            (vseq . m) in ( BoundedFunctions X);

            then ex vseqm be Function of X, REAL st (vseq . m) = vseqm & (vseqm | X) is bounded;

            then

             A35: ( modetrans ((vseq . m),X)) = (vseq . m) by Th19;

            (vseq . k) in ( BoundedFunctions X);

            then ex vseqk be Function of X, REAL st (vseq . k) = vseqk & (vseqk | X) is bounded;

            then

             A36: ( modetrans ((vseq . k),X)) = (vseq . k) by Th19;

            (xseq . m) = (( modetrans ((vseq . m),X)) . x) & (xseq . k) = (( modetrans ((vseq . k),X)) . x) by A28;

            then ((xseq . m) - (xseq . k)) = (h1 . x) by A35, A36, A33, Th34;

            hence thesis by A33, A34, Th26;

          end;

          

           A37: for m be Nat st m >= k holds (rseq . m) <= e

          proof

            let m be Nat;

            assume m >= k;

            then

             A38: ||.((vseq . n) - (vseq . m)).|| < e by A26, A27;

            (rseq . m) = |.((xseq . m) - (xseq . n)).| by A31;

            then (rseq . m) = |.((xseq . n) - (xseq . m)).| by COMPLEX1: 60;

            then (rseq . m) <= ||.((vseq . n) - (vseq . m)).|| by A32;

            hence thesis by A38, XXREAL_0: 2;

          end;

           A39:

          now

            let m be Element of NAT ;

            (wseq . m) = ((xseq . m) + (( - fseq) . m)) by SEQ_1: 7;

            then (wseq . m) = ((xseq . m) + ( - (fseq . m))) by SEQ_1: 10;

            hence (wseq . m) = ((xseq . m) - (xseq . n)) by SEQ_1: 57;

          end;

          now

            let x be object;

            assume x in NAT ;

            then

            reconsider k = x as Element of NAT ;

            (rseq . x) = |.((xseq . k) - (xseq . n)).| by A31;

            then (rseq . x) = |.(wseq . k).| by A39;

            hence (rseq . x) = (( abs wseq) . x) by VALUED_1: 18;

          end;

          then

           A40: rseq = ( abs wseq) by FUNCT_2: 12;

          

           A41: wseq is convergent by A29;

          then rseq is convergent by A40;

          then

           A42: ( lim rseq) <= e by A37, RSSPACE2: 5;

          ( lim fseq) = (fseq . 0 ) by SEQ_4: 26;

          then ( lim fseq) = (xseq . n) by SEQ_1: 57;

          then ( lim wseq) = ((tseq . x) - (xseq . n)) by A29, A30, SEQ_2: 12;

          then ( lim rseq) = |.((tseq . x) - (xseq . n)).| by A41, A40, SEQ_4: 14;

          then |.((xseq . n) - (tseq . x)).| <= e by A42, COMPLEX1: 60;

          hence |.((( modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A28;

        end;

        hence for x be Element of X holds |.((( modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e;

      end;

      

       A43: for e be Real st e > 0 holds ex k be Element of NAT st for n be Element of NAT st n >= k holds ||.((vseq . n) - tv).|| <= e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

         A44: for n be Nat st n >= k holds for x be Element of X holds |.((( modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A25;

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

        take k;

        hereby

          let n be Element of NAT such that

           A45: n >= k;

          (vseq . n) in ( BoundedFunctions X);

          then

          consider f1 be Function of X, REAL such that

           A46: f1 = (vseq . n) and (f1 | X) is bounded;

          ((vseq . n) - tv) in ( BoundedFunctions X);

          then

          consider h1 be Function of X, REAL such that

           A47: h1 = ((vseq . n) - tv) and

           A48: (h1 | X) is bounded;

           A49:

          now

            let t be Element of X;

            ( modetrans ((vseq . n),X)) = f1 & (h1 . t) = ((f1 . t) - (tseq . t)) by A46, A47, Def15, Th34;

            hence |.(h1 . t).| <= e by A44, A45;

          end;

           A50:

          now

            let r be Real;

            assume r in ( PreNorms h1);

            then ex t be Element of X st r = |.(h1 . t).|;

            hence r <= e by A49;

          end;

          (for s be Real st s in ( PreNorms h1) holds s <= e) implies ( upper_bound ( PreNorms h1)) <= e by SEQ_4: 45;

          hence ||.((vseq . n) - tv).|| <= e by A47, A48, A50, Th20;

        end;

      end;

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

      proof

        let e be Real such that

         A51: e > 0 ;

        reconsider ee = e as Real;

        consider m be Element of NAT such that

         A52: for n be Element of NAT st n >= m holds ||.((vseq . n) - tv).|| <= (ee / 2) by A43, A51, XREAL_1: 215;

        take m;

        

         A53: (e / 2) < e by A51, XREAL_1: 216;

        let n be Nat;

        

         A54: n in NAT by ORDINAL1:def 12;

        assume n >= m;

        then ||.((vseq . n) - tv).|| <= (e / 2) by A52, A54;

        hence ||.((vseq . n) - tv).|| < e by A53, XXREAL_0: 2;

      end;

      hence thesis by NORMSP_1:def 6;

    end;

    theorem :: C0SP1:36

    

     Th36: ( R_Normed_Algebra_of_BoundedFunctions X) is RealBanachSpace

    proof

      for seq be sequence of ( R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th35;

      hence thesis by LOPBAN_1:def 15;

    end;

    registration

      let X be non empty set;

      cluster ( R_Normed_Algebra_of_BoundedFunctions X) -> complete;

      coherence by Th36;

    end

    registration

      let X;

      cluster ( R_Normed_Algebra_of_BoundedFunctions X) -> Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 left-distributive left_unital;

      coherence

      proof

        set B = ( R_Normed_Algebra_of_BoundedFunctions X);

        thus B is Banach_Algebra-like_1

        proof

          let f,g be Element of B;

          f in ( BoundedFunctions X);

          then

          consider f1 be Function of X, REAL such that

           A1: f1 = f and

           A2: (f1 | X) is bounded;

          g in ( BoundedFunctions X);

          then

          consider g1 be Function of X, REAL such that

           A3: g1 = g and

           A4: (g1 | X) is bounded;

          

           A5: ( PreNorms g1) is non empty bounded_above by A4, Th17;

          (f * g) in ( BoundedFunctions X);

          then

          consider h1 be Function of X, REAL such that

           A6: h1 = (f * g) and

           A7: (h1 | X) is bounded;

          

           A8: ( PreNorms f1) is non empty bounded_above by A2, Th17;

          now

            let s be Real;

            assume s in ( PreNorms h1);

            then

            consider t be Element of X such that

             A9: s = |.(h1 . t).|;

             |.(g1 . t).| in ( PreNorms g1);

            then

             A10: |.(g1 . t).| <= ( upper_bound ( PreNorms g1)) by A5, SEQ_4:def 1;

             |.(f1 . t).| in ( PreNorms f1);

            then

             A11: |.(f1 . t).| <= ( upper_bound ( PreNorms f1)) by A8, SEQ_4:def 1;

             0 <= |.(f1 . t).| by COMPLEX1: 46;

            then 0 <= ( upper_bound ( PreNorms f1)) by A11;

            then

             A12: (( upper_bound ( PreNorms f1)) * |.(g1 . t).|) <= (( upper_bound ( PreNorms f1)) * ( upper_bound ( PreNorms g1))) by A10, XREAL_1: 64;

             0 <= |.(g1 . t).| by COMPLEX1: 46;

            then

             A13: ( |.(f1 . t).| * |.(g1 . t).|) <= (( upper_bound ( PreNorms f1)) * |.(g1 . t).|) by A11, XREAL_1: 64;

             |.(h1 . t).| = |.((f1 . t) * (g1 . t)).| by A1, A3, A6, Th31;

            then |.(h1 . t).| = ( |.(f1 . t).| * |.(g1 . t).|) by COMPLEX1: 65;

            hence s <= (( upper_bound ( PreNorms f1)) * ( upper_bound ( PreNorms g1))) by A9, A13, A12, XXREAL_0: 2;

          end;

          then

           A14: ( upper_bound ( PreNorms h1)) <= (( upper_bound ( PreNorms f1)) * ( upper_bound ( PreNorms g1))) by SEQ_4: 45;

          

           A15: ||.g.|| = ( upper_bound ( PreNorms g1)) by A3, A4, Th20;

           ||.f.|| = ( upper_bound ( PreNorms f1)) by A1, A2, Th20;

          hence ||.(f * g).|| <= ( ||.f.|| * ||.g.||) by A6, A7, A15, A14, Th20;

        end;

        ( 1. B) in ( BoundedFunctions X);

        then

        consider ONE be Function of X, REAL such that

         A16: ONE = ( 1. B) and

         A17: (ONE | X) is bounded;

        ( 1. B) = ( 1_ ( R_Algebra_of_BoundedFunctions X));

        then

         A18: ( 1. B) = (X --> 1) by Th16;

        for s be object holds s in ( PreNorms ONE) iff s = 1

        proof

          set t = the Element of X;

          let s be object;

          hereby

            assume s in ( PreNorms ONE);

            then

            consider t be Element of X such that

             A20: s = |.(ONE . t).|;

            

             A21: s = |.((X --> 1) . t).| by A16, A18, A20;

            thus s = 1 by A21, COMPLEX1: 48;

          end;

          assume s = 1;

          then s = |.((X --> 1) . t).| by COMPLEX1: 48;

          hence thesis by A16, A18;

        end;

        then ( PreNorms ONE) = {1} by TARSKI:def 1;

        then ( upper_bound ( PreNorms ONE)) = 1 by SEQ_4: 9;

        then ||.( 1. B).|| = 1 by A16, A17, Th20;

        hence B is Banach_Algebra-like_2;

        thus B is Banach_Algebra-like_3

        proof

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

          f in ( BoundedFunctions X);

          then

          consider f1 be Function of X, REAL such that

           A22: f1 = f and (f1 | X) is bounded;

          g in ( BoundedFunctions X);

          then

          consider g1 be Function of X, REAL such that

           A23: g1 = g and (g1 | X) is bounded;

          (a * (f * g)) in ( BoundedFunctions X);

          then

          consider h3 be Function of X, REAL such that

           A24: h3 = (a * (f * g)) and (h3 | X) is bounded;

          (f * g) in ( BoundedFunctions X);

          then

          consider h2 be Function of X, REAL such that

           A25: h2 = (f * g) and (h2 | X) is bounded;

          (a * g) in ( BoundedFunctions X);

          then

          consider h1 be Function of X, REAL such that

           A26: h1 = (a * g) and (h1 | X) is bounded;

          now

            let x be Element of X;

            (h3 . x) = (a * (h2 . x)) by A25, A24, Th30;

            then (h3 . x) = (a * ((f1 . x) * (g1 . x))) by A22, A23, A25, Th31;

            then (h3 . x) = ((f1 . x) * (a * (g1 . x)));

            hence (h3 . x) = ((f1 . x) * (h1 . x)) by A23, A26, Th30;

          end;

          hence (a * (f * g)) = (f * (a * g)) by A22, A26, A24, Th31;

        end;

        thus B is left-distributive

        proof

          let f,g,h be Element of B;

          f in ( BoundedFunctions X);

          then

          consider f1 be Function of X, REAL such that

           A27: f1 = f and (f1 | X) is bounded;

          h in ( BoundedFunctions X);

          then

          consider h1 be Function of X, REAL such that

           A28: h1 = h and (h1 | X) is bounded;

          g in ( BoundedFunctions X);

          then

          consider g1 be Function of X, REAL such that

           A29: g1 = g and (g1 | X) is bounded;

          ((g + h) * f) in ( BoundedFunctions X);

          then

          consider F1 be Function of X, REAL such that

           A30: F1 = ((g + h) * f) and (F1 | X) is bounded;

          (h * f) in ( BoundedFunctions X);

          then

          consider hf1 be Function of X, REAL such that

           A31: hf1 = (h * f) and (hf1 | X) is bounded;

          (g * f) in ( BoundedFunctions X);

          then

          consider gf1 be Function of X, REAL such that

           A32: gf1 = (g * f) and (gf1 | X) is bounded;

          (g + h) in ( BoundedFunctions X);

          then

          consider gPh1 be Function of X, REAL such that

           A33: gPh1 = (g + h) and (gPh1 | X) is bounded;

          now

            let x be Element of X;

            (F1 . x) = ((gPh1 . x) * (f1 . x)) by A27, A33, A30, Th31;

            then (F1 . x) = (((g1 . x) + (h1 . x)) * (f1 . x)) by A29, A28, A33, Th29;

            then (F1 . x) = (((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)));

            then (F1 . x) = ((gf1 . x) + ((h1 . x) * (f1 . x))) by A27, A29, A32, Th31;

            hence (F1 . x) = ((gf1 . x) + (hf1 . x)) by A27, A28, A31, Th31;

          end;

          hence ((g + h) * f) = ((g * f) + (h * f)) by A32, A31, A30, Th29;

        end;

        thus for f be Element of B holds (( 1. B) * f) = f by Lm3;

      end;

    end

    theorem :: C0SP1:37

    ( R_Normed_Algebra_of_BoundedFunctions X) is Banach_Algebra by Th22;