cc0sp1.miz

    begin

    definition

      let V be ComplexAlgebra;

      :: CC0SP1:def1

      mode ComplexSubAlgebra of V -> ComplexAlgebra means

      : Def1: 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 | [: COMPLEX , the carrier of it :]) & ( 1. it ) = ( 1. V) & ( 0. it ) = ( 0. V);

      existence

      proof

        take V;

        thus thesis by RELSET_1: 19;

      end;

    end

     Lm1:

    now

      let z be Complex;

      let X be non empty set, V be ComplexAlgebra, V1 be non empty Subset of V, d1,d2 be Element of X, A be BinOp of X, M be Function of [:X, X:], X, MR be Function of [: COMPLEX , X:], X such that

       A1: V1 = X and

       A2: MR = (the Mult of V | [: COMPLEX , V1:]);

      let W be non empty ComplexAlgebraStr such that

       A3: W = ComplexAlgebraStr (# X, M, A, MR, d2, d1 #);

      let w be VECTOR of W;

      let v be Element of V;

      assume

       A4: w = v;

      z in COMPLEX by XCMPLX_0:def 2;

      then [z, w] in [: COMPLEX , V1:] by A1, A3, ZFMISC_1:def 2;

      hence (z * w) = (z * v) by A4, A2, A3, FUNCT_1: 49;

    end;

    theorem :: CC0SP1:1



     Th1: for X be non empty set, V be ComplexAlgebra, V1 be non empty Subset of V, d1,d2 be Element of X, A be BinOp of X, M be Function of [:X, X:], X, MR be Function of [: COMPLEX , X:], X st (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 | [: COMPLEX , V1:]) & V1 is having-inverse) holds ComplexAlgebraStr (# X, M, A, MR, d2, d1 #) is ComplexSubAlgebra of V

    proof

      let X be non empty set, V be ComplexAlgebra, V1 be non empty Subset of V, d1,d2 be Element of X, A be BinOp of X, M be Function of [:X, X:], X, MR be Function of [: COMPLEX , X:], X;

      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 | [: COMPLEX , V1:]) and

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

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

       A8:

      now

        let x,y be Element of W;

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

        (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: 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 MV = the Mult 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

           A11: (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 A11, RLVECT_1:def 3;

        end;

        hereby

          let x be VECTOR of W;

          reconsider y = x, z = ( 0. W) as VECTOR of V by A1, TARSKI:def 3;



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

          .= x by RLVECT_1: 4;

        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

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

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

          then

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

          take y;

          thus thesis by A2, A8, A12;

        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

           A13: (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 A13, 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

           A14: (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, A14;

        end;

        thus for a be Complex, x,y be VECTOR of W holds (a * (x + y)) = ((a * x) + (a * y))

        proof

          let a be Complex;

          let x,y be VECTOR of W;

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



           A15: (a * x) = (a * x1) by A1, A6, Lm1;



           A16: (a * y) = (a * y1) by A1, A6, Lm1;

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

          then (a * (x + y)) = (a * (x1 + y1)) by A1, A6, Lm1;

          then (a * (x + y)) = ((a * x1) + (a * y1)) by CLVECT_1:def 2;

          hence thesis by A8, A15, A16;

        end;

        thus for a,b be Complex, v be VECTOR of W holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Complex;

          let x be Element of W;

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



           A17: (a * x) = (a * x1) by A1, A6, Lm1;



           A18: (b * x) = (b * x1) by A1, A6, Lm1;

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

          then ((a + b) * x) = ((a * x1) + (b * x1)) by CLVECT_1:def 3;

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

        end;

        thus for a,b be Complex, v be VECTOR of W holds ((a * b) * v) = (a * (b * v))

        proof

          let a,b be Complex;

          let x be Element of W;

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

          reconsider y = (b * x) as Element of W;

          reconsider y1 = (b * x1) as Element of V;



           A19: (b * x) = (b * x1) by A1, A6, Lm1;



           A20: (a * (b * x)) = (a * (b * x1)) by A1, A6, A19, Lm1;

          ((a * b) * x) = ((a * b) * x1) by A1, A6, Lm1;

          hence thesis by A20, CLVECT_1:def 4;

        end;

        thus for x,y be Element of W, a be Complex holds (a * (x * y)) = ((a * x) * y)

        proof

          let x,y be Element of W;

          let a be Complex;

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



           A21: (a * x) = (a * x1) by A1, A6, Lm1;



           A22: (a * (x * y)) = (a * (x1 * y1)) by A1, A6, Lm1, A9;

          (a * (x1 * y1)) = ((a * x1) * y1) by CFUNCDOM:def 9;

          hence thesis by A9, A21, A22;

        end;

        thus thesis;

      end;

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

      hence thesis by A1, A4, A5, A6, A10, Def1;

    end;

    registration

      let V be ComplexAlgebra;

      cluster strict for ComplexSubAlgebra of V;

      existence

      proof

        set V1 = ( [#] V);



         A1: the Mult of V = (the Mult of V | [: COMPLEX , 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 ComplexAlgebraStr (# the carrier of V, the multF of V, the addF of V, the Mult of V, ( 1. V), ( 0. V) #) is ComplexSubAlgebra of V by A1, Th1;

        hence thesis;

      end;

    end

    definition

      let V be ComplexAlgebra, V1 be Subset of V;

      :: CC0SP1:def2

      attr V1 is Cadditively-linearly-closed means

      : Def2: V1 is add-closed having-inverse & for a be Complex, v be Element of V st v in V1 holds (a * v) in V1;

    end

    definition

      let V be ComplexAlgebra, V1 be Subset of V;

      :: CC0SP1:def3

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

      : Def3: (the Mult of V | [: COMPLEX , V1:]);

      correctness

      proof



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



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

        proof

          let z be object such that

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

          consider r,x be object such that

           A5: r in COMPLEX and

           A6: x in V1 and

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

          reconsider r as Complex by A5;

          reconsider y = x as VECTOR of V by A6;

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

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

          hence thesis by A1, A6;

        end;

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

        hence thesis by A3, FUNCT_2: 3;

      end;

    end

    definition

      let X be non empty set;

      :: CC0SP1:def4

      func ComplexBoundedFunctions (X) -> non empty Subset of ( CAlgebra X) equals { f where f be Function of X, COMPLEX : (f | X) is bounded };

      correctness

      proof



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

        proof

          let x be object;

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

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

          hence x in ( Funcs (X, COMPLEX )) by FUNCT_2: 8;

        end;

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

        proof

          reconsider g = (X --> 0c ) as Function of X, COMPLEX ;

          (g | X) is bounded;

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

          hence thesis;

        end;

        hence thesis by A1;

      end;

    end

    registration

      let X be non empty set;

      cluster ( CAlgebra X) -> scalar-unital;

      coherence by CFUNCDOM: 12;

    end

    registration

      let X be non empty set;

      cluster ( ComplexBoundedFunctions X) -> Cadditively-linearly-closed multiplicatively-closed;

      coherence

      proof

        set W = ( ComplexBoundedFunctions X);

        set V = ( CAlgebra X);

        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

           A1: v in W & u in W;

          consider v1 be Function of X, COMPLEX such that

           A2: v1 = v & (v1 | X) is bounded by A1;

          consider u1 be Function of X, COMPLEX such that

           A3: u1 = u & (u1 | X) is bounded by A1;

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

          then

           A4: (v1 + u1) is Function of X, COMPLEX & ((v1 + u1) | X) is bounded by A2, A3, CFUNCT_1: 75;

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



           A5: ex f be Function st h = f & ( dom f) = X & ( rng f) c= COMPLEX by FUNCT_2:def 2;

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

          then

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

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

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

          hence (v + u) in W by A4;

        end;

        then

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

           A8: v in W;

          consider v1 be Function of X, COMPLEX such that

           A9: v1 = v & (v1 | X) is bounded by A8;



           A10: ( - v1) is Function of X, COMPLEX & (( - v1) | X) is bounded by A9, CFUNCT_1: 74;

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



           A11: h = (( - 1r ) * v) by CLVECT_1: 3;



           A12: ex f be Function st h = f & ( dom f) = X & ( rng f) c= COMPLEX by FUNCT_2:def 2;



           A13: ( dom v1) = X by FUNCT_2:def 1;

          now

            let x be object;

            assume x in ( dom h);

            then

            reconsider y = x as Element of X;

            (h . x) = (( - 1r ) * (v2 . y)) by A11, CFUNCDOM: 4;

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

          end;

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

          hence ( - v) in W by A10;

        end;

        then

         A14: W is having-inverse;

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

        proof

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

           A15: u in W;

          consider u1 be Function of X, COMPLEX such that

           A16: u1 = u & (u1 | X) is bounded by A15;



           A17: (a (#) u1) is Function of X, COMPLEX & ((a (#) u1) | X) is bounded by A16, CFUNCT_1: 72;

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



           A18: ex f be Function st h = f & ( dom f) = X & ( rng f) c= COMPLEX by FUNCT_2:def 2;



           A19: ( dom u1) = X by FUNCT_2:def 1;

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

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

          hence (a * u) in W by A17;

        end;

        hence ( ComplexBoundedFunctions X) is Cadditively-linearly-closed by A7, A14;



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

           A21: v in W & u in W;

          consider v1 be Function of X, COMPLEX such that

           A22: v1 = v & (v1 | X) is bounded by A21;

          consider u1 be Function of X, COMPLEX such that

           A23: u1 = u & (u1 | X) is bounded by A21;

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

          then

           A24: (v1 (#) u1) is Function of X, COMPLEX & ((v1 (#) u1) | X) is bounded by A22, A23, CFUNCT_1: 76;

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



           A25: ex f be Function st h = f & ( dom f) = X & ( rng f) c= COMPLEX by FUNCT_2:def 2;

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

          then

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

          for x be object st x in ( dom h) holds (h . x) = ((v1 . x) * (u1 . x)) by A22, A23, CFUNCDOM: 2;

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

          hence (v * u) in W by A24;

        end;

        reconsider g = ( ComplexFuncUnit X) as Function of X, COMPLEX ;

        (g | X) is bounded;

        then ( 1. V) in W;

        hence thesis by A20;

      end;

    end

    registration

      let V be ComplexAlgebra;

      cluster Cadditively-linearly-closed multiplicatively-closed for non empty Subset of V;

      existence

      proof

        reconsider W = ( [#] V) as non empty Subset of V;



         A1: W is Cadditively-linearly-closed;

        W is multiplicatively-closed;

        hence thesis by A1;

      end;

    end

    definition

      let V be non empty CLSStruct;

      :: CC0SP1:def5

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

    end

    theorem :: CC0SP1:2



     Th2: for V be ComplexAlgebra, V1 be Cadditively-linearly-closed multiplicatively-closed non empty Subset of V holds ComplexAlgebraStr (# V1, ( mult_ (V1,V)), ( Add_ (V1,V)), ( Mult_ (V1,V)), ( One_ (V1,V)), ( Zero_ (V1,V)) #) is ComplexSubAlgebra of V

    proof

      let V be ComplexAlgebra, V1 be Cadditively-linearly-closed multiplicatively-closed non empty Subset of V;



       A1: ( Mult_ (V1,V)) = (the Mult of V | [: COMPLEX , V1:]) by Def3;



       A2: V1 is add-closed having-inverse non empty by Def2;



       A3: ( One_ (V1,V)) = ( 1_ V) & ( mult_ (V1,V)) = (the multF of V || V1) by C0SP1:def 6, C0SP1:def 8;

      ( Zero_ (V1,V)) = ( 0. V) & ( Add_ (V1,V)) = (the addF of V || V1) by A2, C0SP1:def 5, C0SP1:def 7;

      hence thesis by A1, A2, A3, Th1;

    end;

    theorem :: CC0SP1:3



     Th3: for V be ComplexAlgebra, V1 be ComplexSubAlgebra 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 Complex st v1 = v holds (a * v1) = (a * v)) & ( 1_ V1) = ( 1_ V) & ( 0. V1) = ( 0. V)

    proof

      let V be ComplexAlgebra, V1 be ComplexSubAlgebra 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 Def1;

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

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

        assume

         A3: v1 = v;

        reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

        (a1 * v1) = ((the Mult of V | [: COMPLEX , the carrier of V1:]) . [a1, v1]) by Def1;

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

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

      end;

      thus thesis by Def1;

    end;

    definition

      let X be non empty set;

      :: CC0SP1:def6

      func C_Algebra_of_BoundedFunctions X -> ComplexAlgebra equals ComplexAlgebraStr (# ( ComplexBoundedFunctions X), ( mult_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( Add_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( Mult_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( One_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( Zero_ (( ComplexBoundedFunctions X),( CAlgebra X))) #);

      coherence by Th2;

    end

    theorem :: CC0SP1:4

    for X be non empty set holds ( C_Algebra_of_BoundedFunctions X) is ComplexSubAlgebra of ( CAlgebra X) by Th2;

    registration

      let X be non empty set;

      cluster ( C_Algebra_of_BoundedFunctions X) -> vector-distributive scalar-unital;

      coherence

      proof

        now

          let v be VECTOR of ( C_Algebra_of_BoundedFunctions X);

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

          ( C_Algebra_of_BoundedFunctions X) is ComplexSubAlgebra of ( CAlgebra X) by Th2;

          then ( 1r * v) = ( 1r * v1) by Th3;

          hence ( 1r * v) = v by CFUNCDOM: 12;

        end;

        hence thesis;

      end;

    end

    theorem :: CC0SP1:5



     Th5: for X be non empty set, F,G,H be VECTOR of ( C_Algebra_of_BoundedFunctions X), f,g,h be Function of X, COMPLEX st f = F & g = G & h = H holds (H = (F + G) iff (for x be Element of X holds (h . x) = ((f . x) + (g . x))))

    proof

      let X be non empty set, F,G,H be VECTOR of ( C_Algebra_of_BoundedFunctions X), f,g,h be Function of X, COMPLEX ;

      assume

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



       A2: ( C_Algebra_of_BoundedFunctions X) is ComplexSubAlgebra of ( CAlgebra X) by Th2;

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

      hereby

        assume

         A3: H = (F + G);

        let x be Element of X;

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

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

      end;

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

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

      hence H = (F + G) by A2, Th3;

    end;

    theorem :: CC0SP1:6



     Th6: for X be non empty set, a be Complex, F,G be VECTOR of ( C_Algebra_of_BoundedFunctions X), f,g be Function of X, COMPLEX st f = F & g = G holds (G = (a * F) iff for x be Element of X holds (g . x) = (a * (f . x)))

    proof

      let X be non empty set, a be Complex, F,G be VECTOR of ( C_Algebra_of_BoundedFunctions X), f,g be Function of X, COMPLEX ;

      assume

       A1: f = F & g = G;



       A2: ( C_Algebra_of_BoundedFunctions X) is ComplexSubAlgebra of ( CAlgebra X) by Th2;

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

      hereby

        assume

         A3: G = (a * F);

        let x be Element of X;

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

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

      end;

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

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

      hence G = (a * F) by A2, Th3;

    end;

    theorem :: CC0SP1:7



     Th7: for X be non empty set, F,G,H be VECTOR of ( C_Algebra_of_BoundedFunctions X), f,g,h be Function of X, COMPLEX st f = F & g = G & h = H holds (H = (F * G) iff for x be Element of X holds (h . x) = ((f . x) * (g . x)))

    proof

      let X be non empty set, F,G,H be VECTOR of ( C_Algebra_of_BoundedFunctions X), f,g,h be Function of X, COMPLEX ;

      assume

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



       A2: ( C_Algebra_of_BoundedFunctions X) is ComplexSubAlgebra of ( CAlgebra X) by Th2;

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

      hereby

        assume

         A3: H = (F * G);

        let x be Element of X;

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

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

      end;

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

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

      hence H = (F * G) by A2, Th3;

    end;

    theorem :: CC0SP1:8



     Th8: for X be non empty set holds ( 0. ( C_Algebra_of_BoundedFunctions X)) = (X --> 0 )

    proof

      let X be non empty set;



       A1: ( C_Algebra_of_BoundedFunctions X) is ComplexSubAlgebra of ( CAlgebra X) by Th2;

      ( 0. ( CAlgebra X)) = (X --> 0 );

      hence thesis by A1, Th3;

    end;

    theorem :: CC0SP1:9



     Th9: for X be non empty set holds ( 1_ ( C_Algebra_of_BoundedFunctions X)) = (X --> 1r )

    proof

      let X be non empty set;



       A1: ( C_Algebra_of_BoundedFunctions X) is ComplexSubAlgebra of ( CAlgebra X) by Th2;

      ( 1_ ( CAlgebra X)) = (X --> 1r );

      hence thesis by A1, Th3;

    end;

    definition

      let X be non empty set, F be object;

      assume

       A1: F in ( ComplexBoundedFunctions X);

      :: CC0SP1:def7

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

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

      correctness by A1;

    end

    definition

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

      :: CC0SP1:def8

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

      coherence

      proof

         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;

        set z = the Element of X;

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

        hence thesis by A1, TARSKI:def 3;

      end;

    end



     Lm2: for C be non empty set, f be PartFunc of C, COMPLEX holds ( |.f.| is bounded iff f is bounded)

    proof

      let C be non empty set, f be PartFunc of C, COMPLEX ;



       A1: ( dom f) = ( dom |.f.|) by VALUED_1:def 11;

      thus |.f.| is bounded implies f is bounded

      proof

        assume |.f.| is bounded;

        then

        consider r1 be Real such that

         A2: for y be set st y in ( dom |.f.|) holds |.( |.f.| . y).| < r1 by COMSEQ_2:def 3;

        now

          let y be set;

          assume

           A3: y in ( dom f);

          then |.( |.f.| . y).| < r1 by A1, A2;

          then |. |.(f . y).|.| < r1 by A1, A3, VALUED_1:def 11;

          hence not r1 <= |.(f . y).|;

        end;

        hence thesis by COMSEQ_2:def 3;

      end;

      assume f is bounded;

      then

      consider r2 be Real such that

       A4: for y be set st y in ( dom f) holds |.(f . y).| < r2 by COMSEQ_2:def 3;

      now

        take r2;

        let y be set;

        assume

         A5: y in ( dom |.f.|);

        then |. |.(f . y).|.| < r2 by A1, A4;

        hence |.( |.f.| . y).| < r2 by A5, VALUED_1:def 11;

      end;

      hence |.f.| is bounded by COMSEQ_2:def 3;

    end;

    theorem :: CC0SP1:10



     Th10: for X be non empty set, f be Function of X, COMPLEX st (f | X) is bounded holds ( PreNorms f) is bounded_above

    proof

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



       A1: ( dom |.f.|) = ( dom f) by VALUED_1:def 11;



       A2: ( dom ( |.f.| | X)) = (X /\ ( dom |.f.|)) by RELAT_1: 61;



       A3: ( |.f.| | X) = |.(f | X).| by RFUNCT_1: 46;

      assume (f | X) is bounded;

      then ( |.f.| | X) is bounded by A3, Lm2;

      then

      consider p be Real such that

       A4: for c be object st c in ( dom ( |.f.| | X)) holds |.(( |.f.| | X) . c).| <= p by RFUNCT_1: 72;

       A5:

      now

        let c be Element of X;

        assume

         A6: c in (X /\ ( dom f));

         |.(( |.f.| | X) . c).| = |.( |.f.| . c).| by A1, A2, A6, FUNCT_1: 47

        .= |. |.(f . c).|.| by VALUED_1: 18;

        hence |.(f . c).| <= p by A1, A2, A4, A6;

      end;



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

       A8:

      now

        let r be ExtReal;

        assume r in ( PreNorms f);

        then

        consider t be Element of X such that

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

        thus r <= p by A7, A9, A5;

      end;

      p is UpperBound of ( PreNorms f) by A8, XXREAL_2:def 1;

      hence thesis by XXREAL_2:def 10;

    end;

    theorem :: CC0SP1:11



     Th11: for X be non empty set, f be Function of X, COMPLEX holds (f | X) is bounded iff ( PreNorms f) is bounded_above

    proof

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

      now

        assume

         A1: ( PreNorms f) is bounded_above;

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

         A2:

        now

          let t be Element of X;

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

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

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

        end;

        take K;

        thus (f | X) is bounded by A2, CFUNCT_1: 69;

      end;

      hence thesis by Th10;

    end;

    definition

      let X be non empty set;

      :: CC0SP1:def9

      func ComplexBoundedFunctionsNorm (X) -> Function of ( ComplexBoundedFunctions X), REAL means

      : Def9: for x be object st x in ( ComplexBoundedFunctions 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 ( ComplexBoundedFunctions X) holds F(z) in REAL by XREAL_0:def 1;

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

        hence thesis;

      end;

      uniqueness

      proof

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

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

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



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

        for z be object st z in ( ComplexBoundedFunctions X) holds (NORM1 . z) = (NORM2 . z)

        proof

          let z be object such that

           A5: z in ( ComplexBoundedFunctions X);

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

          hence thesis by A3, A5;

        end;

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    theorem :: CC0SP1:12



     Th12: for X be non empty set, f be Function of X, COMPLEX st (f | X) is bounded holds ( modetrans (f,X)) = f

    proof

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

      assume (f | X) is bounded;

      then f in ( ComplexBoundedFunctions X);

      hence thesis by Def7;

    end;

    theorem :: CC0SP1:13



     Th13: for X be non empty set, f be Function of X, COMPLEX st (f | X) is bounded holds (( ComplexBoundedFunctionsNorm X) . f) = ( upper_bound ( PreNorms f))

    proof

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

      assume

       A1: (f | X) is bounded;

      then f in ( ComplexBoundedFunctions X);

      then (( ComplexBoundedFunctionsNorm X) . f) = ( upper_bound ( PreNorms ( modetrans (f,X)))) by Def9;

      hence thesis by Th12, A1;

    end;

    definition

      let X be non empty set;

      :: CC0SP1:def10

      func C_Normed_Algebra_of_BoundedFunctions (X) -> Normed_Complex_AlgebraStr equals Normed_Complex_AlgebraStr (# ( ComplexBoundedFunctions X), ( mult_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( Add_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( Mult_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( One_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( Zero_ (( ComplexBoundedFunctions X),( CAlgebra X))), ( ComplexBoundedFunctionsNorm X) #);

      correctness ;

    end

    registration

      let X be non empty set;

      cluster ( C_Normed_Algebra_of_BoundedFunctions X) -> non empty;

      correctness ;

    end

     Lm3:

    now

      let X be non empty set;

      set F = ( C_Normed_Algebra_of_BoundedFunctions X);

      let x,e be Element of ( C_Normed_Algebra_of_BoundedFunctions X);

      set X1 = ( ComplexBoundedFunctions X);

      reconsider f = x as Element of ( ComplexBoundedFunctions X);

      assume

       A1: e = ( One_ (( ComplexBoundedFunctions X),( CAlgebra X)));

      then (x * e) = (( mult_ (( ComplexBoundedFunctions X),( CAlgebra X))) . (f,( 1_ ( CAlgebra X)))) by C0SP1:def 8;

      then

       A2: (x * e) = ((the multF of ( CAlgebra X) || ( ComplexBoundedFunctions X)) . (f,( 1_ ( CAlgebra X)))) by C0SP1:def 6;

      (e * x) = (( mult_ (( ComplexBoundedFunctions X),( CAlgebra X))) . (( 1_ ( CAlgebra X)),f)) by A1, C0SP1:def 8;

      then

       A3: (e * x) = ((the multF of ( CAlgebra X) || ( ComplexBoundedFunctions X)) . (( 1_ ( CAlgebra X)),f)) by C0SP1:def 6;



       A4: ( 1_ ( CAlgebra X)) = ( 1_ ( C_Algebra_of_BoundedFunctions X)) by Th9;

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

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

      hence (x * e) = x;

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

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

      hence (e * x) = x;

    end;

    registration

      let X be non empty set;

      cluster ( C_Normed_Algebra_of_BoundedFunctions X) -> unital;

      correctness

      proof

        reconsider e = ( One_ (( ComplexBoundedFunctions X),( CAlgebra X))) as Element of ( C_Normed_Algebra_of_BoundedFunctions X);

        take e;

        thus thesis by Lm3;

      end;

    end

    theorem :: CC0SP1:14



     Th14: for W be Normed_Complex_AlgebraStr, V be ComplexAlgebra st ComplexAlgebraStr (# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds W is ComplexAlgebra

    proof

      let W be Normed_Complex_AlgebraStr, V be ComplexAlgebra;

      assume

       A1: ComplexAlgebraStr (# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V;

      reconsider W as non empty ComplexAlgebraStr 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 (x * ( 1. W)) = x;

      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 (x * (y + z)) = ((x * y) + (x * z)) 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 x is right_complementable;

      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 ((a * b) * x) = (a * (b * x)) 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 (v * w) = (w * v) 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 ((x + y) + z) = (x + (y + z)) 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 (x + y) = (y + x) by A1;

      end;



       A10: W is vector-distributive

      proof

        let a be Complex;

        let x,y be VECTOR 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 CLVECT_1:def 2;

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

      end;



       A11: W is scalar-distributive

      proof

        let a,b be Complex;

        let x be VECTOR 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 CLVECT_1:def 3;

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

      end;



       A12: W is scalar-associative

      proof

        let a,b be Complex;

        let x be VECTOR 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 CLVECT_1:def 4;

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

      end;



       A13: W is vector-associative

      proof

        let x,y be VECTOR of W;

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

        let a be Complex;

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

        then (a * (x * y)) = ((a * x1) * y1) by CFUNCDOM: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, z = ( 0. W) as VECTOR of V by A1;

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

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

      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;

    theorem :: CC0SP1:15



     Th15: for X be non empty set holds ( C_Normed_Algebra_of_BoundedFunctions X) is ComplexAlgebra

    proof

      let X be non empty set;

      set W = ( C_Normed_Algebra_of_BoundedFunctions X);

      set V = ( C_Algebra_of_BoundedFunctions X);

      ( C_Algebra_of_BoundedFunctions X) is ComplexAlgebra;

      hence thesis by Th14;

    end;

    theorem :: CC0SP1:16

    for X be non empty set, F be Point of ( C_Normed_Algebra_of_BoundedFunctions X) holds (( Mult_ (( ComplexBoundedFunctions X),( CAlgebra X))) . ( 1r ,F)) = F

    proof

      let X be non empty set, F be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

      set X1 = ( ComplexBoundedFunctions X);

      reconsider f1 = F as Element of ( ComplexBoundedFunctions X);



       A1: [ 1r , f1] in [: COMPLEX , ( ComplexBoundedFunctions X):];

      (( Mult_ (( ComplexBoundedFunctions X),( CAlgebra X))) . ( 1r ,F)) = ((the Mult of ( CAlgebra X) | [: COMPLEX , ( ComplexBoundedFunctions X):]) . ( 1r ,f1)) by Def3

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

      .= F by CFUNCDOM: 12;

      hence thesis;

    end;

    theorem :: CC0SP1:17



     Th17: for X be non empty set holds ( C_Normed_Algebra_of_BoundedFunctions X) is ComplexLinearSpace

    proof

      let X be non empty set;

      for v be Point of ( C_Normed_Algebra_of_BoundedFunctions X) holds ( 1r * v) = v

      proof

        let v be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

        reconsider v1 = v as Element of ( ComplexBoundedFunctions X);



         A1: ( 1r * v) = ((the Mult of ( CAlgebra X) | [: COMPLEX , ( ComplexBoundedFunctions X):]) . [ 1r , v1]) by Def3

        .= (the Mult of ( CAlgebra X) . ( 1r ,v1)) by FUNCT_1: 49

        .= v1 by CFUNCDOM: 12;

        thus thesis by A1;

      end;

      hence thesis by Th15, CLVECT_1:def 5;

    end;

    theorem :: CC0SP1:18



     Th18: for X be non empty set holds (X --> 0 ) = ( 0. ( C_Normed_Algebra_of_BoundedFunctions X))

    proof

      let X be non empty set;

      (X --> 0 ) = ( 0. ( C_Algebra_of_BoundedFunctions X)) by Th8;

      hence thesis;

    end;

    theorem :: CC0SP1:19



     Th19: for X be non empty set, x be Element of X, f be Function of X, COMPLEX , F be Point of ( C_Normed_Algebra_of_BoundedFunctions X) st f = F & (f | X) is bounded holds |.(f . x).| <= ||.F.||

    proof

      let X be non empty set, x be Element of X, f be Function of X, COMPLEX , F be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

      assume that

       A1: f = F and

       A2: (f | X) is bounded;

      reconsider r = |.(f . x).| as ExtReal;



       A3: r in ( PreNorms f);

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

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

      hence |.(f . x).| <= ||.F.|| by A1, A2, Th13;

    end;

    theorem :: CC0SP1:20

    for X be non empty set, F be Point of ( C_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

    proof

      let X be non empty set, F be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

      F in ( ComplexBoundedFunctions X);

      then

      consider g be Function of X, COMPLEX such that

       A1: F = g and

       A2: (g | X) is bounded;

      consider r0 be object such that

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

      reconsider r1 = r0 as Real by A3;

      now

        let r be Real;

        assume r in ( PreNorms g);

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

        hence 0 <= r;

      end;

      then

       A4: 0 <= r1 by A3;

      ( PreNorms g) is non empty bounded_above by Th11, A2;

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

      hence 0 <= ||.F.|| by A1, A2, Th13;

    end;

    theorem :: CC0SP1:21



     Th21: for X be non empty set, F be Point of ( C_Normed_Algebra_of_BoundedFunctions X) st F = ( 0. ( C_Normed_Algebra_of_BoundedFunctions X)) holds 0 = ||.F.||

    proof

      let X be non empty set, F be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

      set z = (X --> 0 );

      reconsider z = (X --> 0c ) as Function of X, COMPLEX ;

      F in ( ComplexBoundedFunctions X);

      then

      consider g be Function of X, COMPLEX such that

       A1: g = F and

       A2: (g | X) is bounded;



       A3: ( not ( PreNorms g) is empty & ( PreNorms g) is bounded_above) by A2, Th11;

      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. ( C_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, Th18;



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

        .= 0 ;

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

      end;

      then 0 <= r0 by A4;

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

      hence 0 = ||.F.|| by A1, A2, Th13;

    end;

    theorem :: CC0SP1:22



     Th22: for X be non empty set, f,g,h be Function of X, COMPLEX , F,G,H be Point of ( C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds (H = (F + G) iff for x be Element of X holds (h . x) = ((f . x) + (g . x)))

    proof

      let X be non empty set, f,g,h be Function of X, COMPLEX , F,G,H be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

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



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

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

      hence thesis by A1, Th5;

    end;

    theorem :: CC0SP1:23



     Th23: for X be non empty set, a be Complex, f,g be Function of X, COMPLEX , F,G be Point of ( C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds (G = (a * F) iff for x be Element of X holds (g . x) = (a * (f . x)))

    proof

      let X be non empty set, a be Complex, f,g be Function of X, COMPLEX , F,G be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

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



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

      assume f = F & g = G;

      hence thesis by A1, Th6;

    end;

    theorem :: CC0SP1:24



     Th24: for X be non empty set, f,g,h be Function of X, COMPLEX , F,G,H be Point of ( C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds (H = (F * G) iff for x be Element of X holds (h . x) = ((f . x) * (g . x)))

    proof

      let X be non empty set, f,g,h be Function of X, COMPLEX , F,G,H be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

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



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

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

      hence thesis by A1, Th7;

    end;

    theorem :: CC0SP1:25



     Th25: for X be non empty set, a be Complex, F,G be Point of ( C_Normed_Algebra_of_BoundedFunctions X) holds (( ||.F.|| = 0 implies F = ( 0. ( C_Normed_Algebra_of_BoundedFunctions X))) & (F = ( 0. ( C_Normed_Algebra_of_BoundedFunctions X)) implies ||.F.|| = 0 ) & ||.(a * F).|| = ( |.a.| * ||.F.||) & ||.(F + G).|| <= ( ||.F.|| + ||.G.||))

    proof

      let X be non empty set, a be Complex, F,G be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

       A1:

      now

        set z = (X --> 0c );

        reconsider z = (X --> 0c ) as Function of X, COMPLEX ;

        F in ( ComplexBoundedFunctions X);

        then

        consider g be Function of X, COMPLEX such that

         A2: F = g and

         A3: (g | X) is bounded;



         A4: not ( PreNorms g) is empty & ( PreNorms g) is bounded_above by A3, Th11;

        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. ( C_Normed_Algebra_of_BoundedFunctions X));

        then

         A7: z = g by A2, Th18;

         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 ;

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

        end;

        then 0 <= r0 by A5;

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

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

      end;



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

      proof

        (F + G) in ( ComplexBoundedFunctions X);

        then

        consider h1 be Function of X, COMPLEX such that

         A11: h1 = (F + G) and

         A12: (h1 | X) is bounded;

        G in ( ComplexBoundedFunctions X);

        then

        consider g1 be Function of X, COMPLEX such that

         A13: g1 = G and

         A14: (g1 | X) is bounded;

        F in ( ComplexBoundedFunctions X);

        then

        consider f1 be Function of X, COMPLEX 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, Th19;

          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, Th22, 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 ||.(F + G).|| <= ( ||.F.|| + ||.G.||) by A11, A12, A19, Th13;

      end;



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

      proof

        F in ( ComplexBoundedFunctions X);

        then

        consider f1 be Function of X, COMPLEX such that

         A21: f1 = F and

         A22: (f1 | X) is bounded;

        (a * F) in ( ComplexBoundedFunctions X);

        then

        consider h1 be Function of X, COMPLEX 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, Th23;

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

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

        end;

         A26:

        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

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

        per cases ;

          suppose

           A28: a <> 0 ;

           A29:

          now

            let t be Element of X;

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

            then

             A30: |.(a " ).| = (1 / |.a.|) by COMPLEX1: 80;

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

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

            then

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

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

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

          end;

           A32:

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

          end;

          (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, A32, Th13;

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

          then ( |.a.| * ||.F.||) <= (( |.a.| * ( |.a.| " )) * ||.(a * F).||);

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

          hence ||.(a * F).|| = ( |.a.| * ||.F.||) by A27, XXREAL_0: 1;

        end;

          suppose

           A33: a = 0 ;

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

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

          .= ((a * fz) + (a * fz)) by CLVECT_1:def 3;

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

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

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

          then

           A34: (a * F) = ( 0. ( C_Normed_Algebra_of_BoundedFunctions X)) by RLVECT_1: 4;

          ( |.a.| * ||.F.||) = ( 0 * ||.F.||) by A33;

          hence ||.(a * F).|| = ( |.a.| * ||.F.||) by A34, Th21;

        end;

      end;

      now

        set z = (X --> 0c );

        reconsider z = (X --> 0c ) as Function of X, COMPLEX ;

        F in ( ComplexBoundedFunctions X);

        then

        consider g be Function of X, COMPLEX such that

         A35: F = g and

         A36: (g | X) is bounded;

        assume

         A37: ||.F.|| = 0 ;

        now

          let t be Element of X;

           |.(g . t).| = 0 by A35, A36, A37, Th19;



          hence (g . t) = 0

          .= (z . t);

        end;

        then g = z by FUNCT_2: 63;

        hence F = ( 0. ( C_Normed_Algebra_of_BoundedFunctions X)) by A35, Th18;

      end;

      hence thesis by A1, A20, A10;

    end;



     Lm4: for X be non empty set holds ( C_Normed_Algebra_of_BoundedFunctions X) is reflexive discerning ComplexNormSpace-like by Th25;

    registration

      let X be non empty set;

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

      coherence by Th17, Lm4;

    end

    theorem :: CC0SP1:26



     Th26: for X be non empty set, f,g,h be Function of X, COMPLEX , F,G,H be Point of ( C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds (H = (F - G) iff for x be Element of X holds (h . x) = ((f . x) - (g . x)))

    proof

      let X be non empty set, f,g,h be Function of X, COMPLEX , F,G,H be Point of ( C_Normed_Algebra_of_BoundedFunctions X);

      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, Th22;

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

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

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

      end;

      now

        assume H = (F - G);

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

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

        then

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

        now

          let x be Element of X;

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

          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 :: CC0SP1:27



     Th27: for X be non empty set, seq be sequence of ( C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds seq is convergent

    proof

      let X be non empty set, vseq be sequence of ( C_Normed_Algebra_of_BoundedFunctions X);

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

      assume

       A1: vseq is CCauchy;



       A2: for x be Element of X holds ex y be Element of COMPLEX st S1[x, y]

      proof

        let x be Element of X;

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

        consider xseq be Complex_Sequence such that

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



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

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A3;

        end;

        reconsider y = ( lim xseq) as Element of COMPLEX by XCMPLX_0:def 2;

        take y;



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

        proof

          let m,k be Nat;



           A6: m in NAT & k in NAT by ORDINAL1:def 12;

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

          then

          consider h1 be Function of X, COMPLEX such that

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

           A8: (h1 | X) is bounded;

          (vseq . m) in ( ComplexBoundedFunctions X);

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

          then

           A9: ( modetrans ((vseq . m),X)) = (vseq . m) by Th12;

          (vseq . k) in ( ComplexBoundedFunctions X);

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

          then

           A10: ( modetrans ((vseq . k),X)) = (vseq . k) by Th12;

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

          then ((xseq . m) - (xseq . k)) = (h1 . x) by A9, A10, A7, Th26;

          hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A7, A8, Th19;

        end;

        now

          let e be Real;

          assume e > 0 ;

          then

          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, CSSPACE3: 8;

          reconsider k as Nat;

          take k;

          hereby

            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;

        end;

        then xseq is convergent by COMSEQ_3: 46;

        hence S1[x, y] by A4;

      end;

      consider tseq be Function of X, COMPLEX such that

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

      now

        let e1 be Real;

        assume

         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, CSSPACE3: 8;

        take k;

        now

          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 CLVECT_1: 110, NORMSP_0:def 4;

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

        end;

        hence for m be Nat st m >= k holds |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1;

      end;

      then

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

      now

        let x be set;

        assume

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

        then

        consider xseq be Complex_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 ( |.xseq.| . n) <= ( ||.vseq.|| . n)

        proof

          let n be Nat;



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

          (vseq . n) in ( ComplexBoundedFunctions X);

          then

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

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

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

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

          hence ( |.xseq.| . n) <= ( ||.vseq.|| . n) by NORMSP_0:def 4;

        end;

        ( |.xseq.| is convergent & |.(tseq . x).| = ( lim |.xseq.|)) by A21, SEQ_2: 27;

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

      end;

      then for x be Element of X st x in (X /\ ( dom tseq)) holds |.(tseq /. x).| <= ( lim ||.vseq.||);

      then (tseq | X) is bounded by CFUNCT_1: 69;

      then tseq in ( ComplexBoundedFunctions X);

      then

      reconsider tv = tseq as Point of ( C_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, CSSPACE3: 8;

        take k;

        now

          let n be Nat;

          assume

           A27: n >= k;

          now

            let x be Element of X;

            consider xseq be Complex_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 xn = (xseq . n) as Element of COMPLEX by XCMPLX_0:def 2;

            reconsider fseq = ( NAT --> xn) as Complex_Sequence;

            set wseq = (xseq - fseq);

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

            consider rseq be Real_Sequence such that

             A31: for m be Nat holds (rseq . m) = H1(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 ( ComplexBoundedFunctions X);

              then

              consider h1 be Function of X, COMPLEX such that

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

               A34: (h1 | X) is bounded;

              (vseq . m) in ( ComplexBoundedFunctions X);

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

              then

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

              (vseq . k) in ( ComplexBoundedFunctions X);

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

              then

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

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

              hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A33, A34, Th19;

            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 (rseq . m) <= e by A38, XXREAL_0: 2;

            end;

             A39:

            now

              let m be Element of NAT ;

              ((xseq - fseq) . m) = ((xseq . m) + (( - fseq) . m)) by VALUED_1: 1

              .= ((xseq . m) - (fseq . m)) by VALUED_1: 8;

              hence ((xseq - fseq) . m) = ((xseq . m) - (xseq . n));

            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) = |.((xseq - fseq) . k).| by A39;

              hence (rseq . x) = ( |.(xseq - fseq).| . x) by VALUED_1: 18;

            end;

            then

             A40: rseq = |.(xseq - fseq).| by FUNCT_2: 12;



             A41: fseq is convergent by CFCONT_1: 26;



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

            ( lim fseq) = (fseq . 0 ) by CFCONT_1: 28;

            then ( lim fseq) = (xseq . n);

            then ( lim (xseq - fseq)) = ((tseq . x) - (xseq . n)) by A29, A30, A41, COMSEQ_2: 26;

            then ( lim rseq) = |.((tseq . x) - (xseq . n)).| by A41, A29, A40, SEQ_2: 27;

            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;

        hence for n be Nat st n >= k holds 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 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

         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;

        take k;

        hereby

          let n be Nat;

          assume

           A45: n >= k;

          (vseq . n) in ( ComplexBoundedFunctions X);

          then

          consider f1 be Function of X, COMPLEX such that

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

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

          then

          consider h1 be Function of X, COMPLEX 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, Def7, Th26;

            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, Th13;

        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;

        assume

         A51: e > 0 ;

        consider m be Nat such that

         A52: for n be Nat st n >= m holds ||.((vseq . n) - tv).|| <= (e / 2) by A43, A51;

        take m;



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

        hereby

          let n be Nat;

          assume n >= m;

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

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

        end;

      end;

      hence thesis;

    end;

    registration

      let X be non empty set;

      cluster ( C_Normed_Algebra_of_BoundedFunctions X) -> complete;

      coherence

      proof

        for seq be sequence of ( C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds seq is convergent by Th27;

        hence thesis by CLOPBAN1:def 13;

      end;

    end

    theorem :: CC0SP1:28

    for X be non empty set holds ( C_Normed_Algebra_of_BoundedFunctions X) is Complex_Banach_Algebra

    proof

      let X be non empty set;

      set B = ( C_Normed_Algebra_of_BoundedFunctions X);

      reconsider B = ( C_Normed_Algebra_of_BoundedFunctions X) as non empty Normed_Complex_Algebra by Th15;

      set X1 = ( ComplexBoundedFunctions X);

      ( 1. B) in ( ComplexBoundedFunctions X);

      then

      consider ONE be Function of X, COMPLEX such that

       A1: ONE = ( 1. B) and

       A2: (ONE | X) is bounded;

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

      then

       A3: ( 1. B) = (X --> 1r ) by Th9;

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

      proof

        set t = the Element of X;

        let s be object;



         A4: ((X --> 1) . t) = 1;

        hereby

          assume s in ( PreNorms ONE);

          then

          consider t be Element of X such that

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

          thus s = 1 by A5, COMPLEX1: 48, A1, A3;

        end;

        assume s = 1;

        hence s in ( PreNorms ONE) by A1, A3, A4, COMPLEX1: 48;

      end;

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

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

      then

       A6: ||.( 1. B).|| = 1 by A1, A2, Th13;

       A7:

      now

        let a be Complex;

        let f,g be Element of B;

        f in ( ComplexBoundedFunctions X);

        then

        consider f1 be Function of X, COMPLEX such that

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

        g in ( ComplexBoundedFunctions X);

        then

        consider g1 be Function of X, COMPLEX such that

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

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

        then

        consider h3 be Function of X, COMPLEX such that

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

        (f * g) in ( ComplexBoundedFunctions X);

        then

        consider h2 be Function of X, COMPLEX such that

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

        (a * g) in ( ComplexBoundedFunctions X);

        then

        consider h1 be Function of X, COMPLEX such that

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

        now

          let x be Element of X;

          (h3 . x) = (a * (h2 . x)) by A11, A10, Th23;

          then (h3 . x) = (a * ((f1 . x) * (g1 . x))) by A8, A9, A11, Th24;

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

          hence (h3 . x) = ((f1 . x) * (h1 . x)) by A9, A12, Th23;

        end;

        hence (a * (f * g)) = (f * (a * g)) by A8, A12, A10, Th24;

      end;

       A13:

      now

        let f,g be Element of B;

        f in ( ComplexBoundedFunctions X);

        then

        consider f1 be Function of X, COMPLEX such that

         A14: f1 = f and

         A15: (f1 | X) is bounded;

        g in ( ComplexBoundedFunctions X);

        then

        consider g1 be Function of X, COMPLEX such that

         A16: g1 = g and

         A17: (g1 | X) is bounded;



         A18: ( not ( PreNorms g1) is empty & ( PreNorms g1) is bounded_above) by A17, Th10;

        (f * g) in ( ComplexBoundedFunctions X);

        then

        consider h1 be Function of X, COMPLEX such that

         A19: h1 = (f * g) and

         A20: (h1 | X) is bounded;



         A21: not ( PreNorms f1) is empty & ( PreNorms f1) is bounded_above by A15, Th10;

        now

          let s be Real;

          assume s in ( PreNorms h1);

          then

          consider t be Element of X such that

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

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

          then

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

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

          then

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

          then

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



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

           |.(h1 . t).| = |.((f1 . t) * (g1 . t)).| by A14, A16, A19, Th24;

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

          hence s <= (( upper_bound ( PreNorms f1)) * ( upper_bound ( PreNorms g1))) by A22, A26, A25, XXREAL_0: 2;

        end;

        then

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



         A28: ||.g.|| = ( upper_bound ( PreNorms g1)) by A16, A17, Th13;

         ||.f.|| = ( upper_bound ( PreNorms f1)) by A14, A15, Th13;

        hence ||.(f * g).|| <= ( ||.f.|| * ||.g.||) by A19, A20, A28, A27, Th13;

      end;

       A29:

      now

        let f,g,h be Element of B;

        f in ( ComplexBoundedFunctions X);

        then

        consider f1 be Function of X, COMPLEX such that

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

        h in ( ComplexBoundedFunctions X);

        then

        consider h1 be Function of X, COMPLEX such that

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

        g in ( ComplexBoundedFunctions X);

        then

        consider g1 be Function of X, COMPLEX such that

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

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

        then

        consider F1 be Function of X, COMPLEX such that

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

        (h * f) in ( ComplexBoundedFunctions X);

        then

        consider hf1 be Function of X, COMPLEX such that

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

        (g * f) in ( ComplexBoundedFunctions X);

        then

        consider gf1 be Function of X, COMPLEX such that

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

        (g + h) in ( ComplexBoundedFunctions X);

        then

        consider gPh1 be Function of X, COMPLEX such that

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

        now

          let x be Element of X;

          (F1 . x) = ((gPh1 . x) * (f1 . x)) by A30, A36, A33, Th24;

          then (F1 . x) = (((g1 . x) + (h1 . x)) * (f1 . x)) by A32, A31, A36, Th22;

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

          then (F1 . x) = ((gf1 . x) + ((h1 . x) * (f1 . x))) by A30, A32, A35, Th24;

          hence (F1 . x) = ((gf1 . x) + (hf1 . x)) by A30, A31, A34, Th24;

        end;

        hence ((g + h) * f) = ((g * f) + (h * f)) by A35, A34, A33, Th22;

      end;

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

      then

       A37: B is left_unital;



       A38: B is Banach_Algebra-like_1 by A13, CLOPBAN2:def 9;



       A39: B is Banach_Algebra-like_2 by A6, CLOPBAN2:def 10;



       A40: B is Banach_Algebra-like_3 by A7, CLOPBAN2:def 11;

      B is left-distributive by A29;

      hence thesis by A37, A38, A39, A40;

    end;