clopban1.miz



    begin

    definition

      let X be set;

      let Y be non empty set;

      let F be Function of [: COMPLEX , Y:], Y;

      let c be Complex, f be Function of X, Y;

      :: original: [;]

      redefine

      func F [;] (c,f) -> Element of ( Funcs (X,Y)) ;

      coherence

      proof

        

         A1: ( dom f) = X by FUNCT_2:def 1;

        c in COMPLEX by XCMPLX_0:def 2;

        then (( dom f) --> c) is Function of X, COMPLEX by A1, FUNCOP_1: 45;

        then

        reconsider g = <:(( dom f) --> c), f:> as Function of X, [: COMPLEX , Y:] by FUNCT_3: 58;

        (F [;] (c,f)) = (F * g) by FUNCOP_1:def 5;

        hence thesis by FUNCT_2: 8;

      end;

    end

    definition

      let X be non empty set;

      let Y be ComplexLinearSpace;

      :: CLOPBAN1:def1

      func FuncExtMult (X,Y) -> Function of [: COMPLEX , ( Funcs (X,the carrier of Y)):], ( Funcs (X,the carrier of Y)) means

      : Def1: for c be Complex, f be Element of ( Funcs (X,the carrier of Y)), x be Element of X holds ((it . [c, f]) . x) = (c * (f . x));

      existence

      proof

        deffunc F( Complex, Element of ( Funcs (X,the carrier of Y))) = (the Mult of Y [;] ($1,$2));

        consider F be Function of [: COMPLEX , ( Funcs (X,the carrier of Y)):], ( Funcs (X,the carrier of Y)) such that

         A1: for c be Element of COMPLEX , f be Element of ( Funcs (X,the carrier of Y)) holds (F . (c,f)) = F(c,f) from BINOP_1:sch 4;

        take F;

        let c be Complex, f be Element of ( Funcs (X,the carrier of Y)), x be Element of X;

        reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;

        

         A2: ( dom (F . [c1, f])) = X by FUNCT_2: 92;

        (F . (c1,f)) = (the Mult of Y [;] (c1,f)) by A1;

        

        hence ((F . [c, f]) . x) = (the Mult of Y . (c,(f . x))) by A2, FUNCOP_1: 32

        .= (c * (f . x)) by CLVECT_1:def 1;

      end;

      uniqueness

      proof

        let it1,it2 be Function of [: COMPLEX , ( Funcs (X,the carrier of Y)):], ( Funcs (X,the carrier of Y)) such that

         A3: for c be Complex, f be Element of ( Funcs (X,the carrier of Y)), x be Element of X holds ((it1 . [c, f]) . x) = (c * (f . x)) and

         A4: for c be Complex, f be Element of ( Funcs (X,the carrier of Y)), x be Element of X holds ((it2 . [c, f]) . x) = (c * (f . x));

        now

          let c be Element of COMPLEX , f be Element of ( Funcs (X,the carrier of Y));

          now

            let x be Element of X;

            

            thus ((it1 . [c, f]) . x) = (c * (f . x)) by A3

            .= ((it2 . [c, f]) . x) by A4;

          end;

          hence (it1 . (c,f)) = (it2 . (c,f)) by FUNCT_2: 63;

        end;

        hence thesis;

      end;

    end

    reserve X for non empty set;

    reserve Y for ComplexLinearSpace;

    reserve f,g,h for Element of ( Funcs (X,the carrier of Y));

    theorem :: CLOPBAN1:1

    

     Th1: for x be Element of X holds (( FuncZero (X,Y)) . x) = ( 0. Y)

    proof

      let x be Element of X;

      

      thus (( FuncZero (X,Y)) . x) = ((X --> ( 0. Y)) . x) by LOPBAN_1:def 3

      .= ( 0. Y) by FUNCOP_1: 7;

    end;

    reserve a,b for Complex;

    theorem :: CLOPBAN1:2

    

     Th2: h = (( FuncExtMult (X,Y)) . [a, f]) iff for x be Element of X holds (h . x) = (a * (f . x))

    proof

      thus h = (( FuncExtMult (X,Y)) . [a, f]) implies for x be Element of X holds (h . x) = (a * (f . x)) by Def1;

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

      now

        assume

         A1: for x be Element of X holds (h . x) = (a * (f . x));

        for x be Element of X holds (h . x) = ((( FuncExtMult (X,Y)) . [a, f]) . x)

        proof

          let x be Element of X;

          

          thus (h . x) = (a * (f . x)) by A1

          .= ((( FuncExtMult (X,Y)) . [a, f]) . x) by Def1;

        end;

        hence h = (( FuncExtMult (X,Y)) . [a, f]) by FUNCT_2: 63;

      end;

      hence thesis;

    end;

    reserve u,v,w for VECTOR of CLSStruct (# ( Funcs (X,the carrier of Y)), ( FuncZero (X,Y)), ( FuncAdd (X,Y)), ( FuncExtMult (X,Y)) #);

    theorem :: CLOPBAN1:3

    

     Th3: (( FuncAdd (X,Y)) . (f,g)) = (( FuncAdd (X,Y)) . (g,f))

    proof

      now

        let x be Element of X;

        

        thus ((( FuncAdd (X,Y)) . (f,g)) . x) = ((g . x) + (f . x)) by LOPBAN_1: 1

        .= ((( FuncAdd (X,Y)) . (g,f)) . x) by LOPBAN_1: 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLOPBAN1:4

    

     Th4: (( FuncAdd (X,Y)) . (f,(( FuncAdd (X,Y)) . (g,h)))) = (( FuncAdd (X,Y)) . ((( FuncAdd (X,Y)) . (f,g)),h))

    proof

      now

        let x be Element of X;

        

        thus ((( FuncAdd (X,Y)) . (f,(( FuncAdd (X,Y)) . (g,h)))) . x) = ((f . x) + ((( FuncAdd (X,Y)) . (g,h)) . x)) by LOPBAN_1: 1

        .= ((f . x) + ((g . x) + (h . x))) by LOPBAN_1: 1

        .= (((f . x) + (g . x)) + (h . x)) by RLVECT_1:def 3

        .= (((( FuncAdd (X,Y)) . (f,g)) . x) + (h . x)) by LOPBAN_1: 1

        .= ((( FuncAdd (X,Y)) . ((( FuncAdd (X,Y)) . (f,g)),h)) . x) by LOPBAN_1: 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLOPBAN1:5

    

     Th5: (( FuncAdd (X,Y)) . (( FuncZero (X,Y)),f)) = f

    proof

      now

        let x be Element of X;

        

        thus ((( FuncAdd (X,Y)) . (( FuncZero (X,Y)),f)) . x) = ((( FuncZero (X,Y)) . x) + (f . x)) by LOPBAN_1: 1

        .= (( 0. Y) + (f . x)) by Th1

        .= (f . x) by RLVECT_1:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLOPBAN1:6

    

     Th6: (( FuncAdd (X,Y)) . (f,(( FuncExtMult (X,Y)) . [( - 1r ), f]))) = ( FuncZero (X,Y))

    proof

      reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of X;

        set y = (f . x);

        

        thus ((( FuncAdd (X,Y)) . (f,(( FuncExtMult (X,Y)) . [mj, f]))) . x) = ((f . x) + ((( FuncExtMult (X,Y)) . [mj, f]) . x)) by LOPBAN_1: 1

        .= ((f . x) + (( - 1r ) * y)) by Th2

        .= ((f . x) + ( - y)) by CLVECT_1: 3

        .= ( 0. Y) by RLVECT_1: 5

        .= (( FuncZero (X,Y)) . x) by Th1;

      end;

      then (( FuncAdd (X,Y)) . (f,(( FuncExtMult (X,Y)) . [mj, f]))) = ( FuncZero (X,Y)) by FUNCT_2: 63;

      hence thesis;

    end;

    theorem :: CLOPBAN1:7

    

     Th7: (( FuncExtMult (X,Y)) . [ 1r , f]) = f

    proof

      now

        let x be Element of X;

        

        thus ((( FuncExtMult (X,Y)) . [ 1r , f]) . x) = ( 1r * (f . x)) by Th2

        .= (f . x) by CLVECT_1:def 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLOPBAN1:8

    

     Th8: (( FuncExtMult (X,Y)) . [a, (( FuncExtMult (X,Y)) . [b, f])]) = (( FuncExtMult (X,Y)) . [(a * b), f])

    proof

      reconsider a1 = a, b1 = b, ab = (a * b) as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of X;

        

        thus ((( FuncExtMult (X,Y)) . [a1, (( FuncExtMult (X,Y)) . [b1, f])]) . x) = (a1 * ((( FuncExtMult (X,Y)) . [b1, f]) . x)) by Th2

        .= (a * (b * (f . x))) by Th2

        .= ((a * b) * (f . x)) by CLVECT_1:def 4

        .= ((( FuncExtMult (X,Y)) . [ab, f]) . x) by Th2;

      end;

      then (( FuncExtMult (X,Y)) . [a, (( FuncExtMult (X,Y)) . [b, f])]) = (( FuncExtMult (X,Y)) . [ab, f]) by FUNCT_2: 63;

      hence thesis;

    end;

    theorem :: CLOPBAN1:9

    

     Th9: (( FuncAdd (X,Y)) . ((( FuncExtMult (X,Y)) . [a, f]),(( FuncExtMult (X,Y)) . [b, f]))) = (( FuncExtMult (X,Y)) . [(a + b), f])

    proof

      reconsider a1 = a, b1 = b, ab = (a + b) as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of X;

        

        thus ((( FuncAdd (X,Y)) . ((( FuncExtMult (X,Y)) . [a1, f]),(( FuncExtMult (X,Y)) . [b1, f]))) . x) = (((( FuncExtMult (X,Y)) . [a1, f]) . x) + ((( FuncExtMult (X,Y)) . [b1, f]) . x)) by LOPBAN_1: 1

        .= ((a1 * (f . x)) + ((( FuncExtMult (X,Y)) . [b1, f]) . x)) by Th2

        .= ((a * (f . x)) + (b * (f . x))) by Th2

        .= ((a + b) * (f . x)) by CLVECT_1:def 3

        .= ((( FuncExtMult (X,Y)) . [ab, f]) . x) by Th2;

      end;

      then (( FuncAdd (X,Y)) . ((( FuncExtMult (X,Y)) . [a, f]),(( FuncExtMult (X,Y)) . [b, f]))) = (( FuncExtMult (X,Y)) . [(a + b), f]) by FUNCT_2: 63;

      hence thesis;

    end;

    

     Lm1: (( FuncAdd (X,Y)) . ((( FuncExtMult (X,Y)) . [a, f]),(( FuncExtMult (X,Y)) . [a, g]))) = (( FuncExtMult (X,Y)) . [a, (( FuncAdd (X,Y)) . (f,g))])

    proof

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

      now

        let x be Element of X;

        

        thus ((( FuncAdd (X,Y)) . ((( FuncExtMult (X,Y)) . [a1, f]),(( FuncExtMult (X,Y)) . [a1, g]))) . x) = (((( FuncExtMult (X,Y)) . [a1, f]) . x) + ((( FuncExtMult (X,Y)) . [a1, g]) . x)) by LOPBAN_1: 1

        .= ((a1 * (f . x)) + ((( FuncExtMult (X,Y)) . [a1, g]) . x)) by Th2

        .= ((a * (f . x)) + (a * (g . x))) by Th2

        .= (a * ((f . x) + (g . x))) by CLVECT_1:def 2

        .= (a * ((( FuncAdd (X,Y)) . (f,g)) . x)) by LOPBAN_1: 1

        .= ((( FuncExtMult (X,Y)) . [a1, (( FuncAdd (X,Y)) . (f,g))]) . x) by Th2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLOPBAN1:10

    

     Th10: CLSStruct (# ( Funcs (X,the carrier of Y)), ( FuncZero (X,Y)), ( FuncAdd (X,Y)), ( FuncExtMult (X,Y)) #) is ComplexLinearSpace

    proof

      set IT = CLSStruct (# ( Funcs (X,the carrier of Y)), ( FuncZero (X,Y)), ( FuncAdd (X,Y)), ( FuncExtMult (X,Y)) #);

      

       A1: ((u + v) + w) = (u + (v + w)) by Th4;

      

       A2: u is right_complementable

      proof

        reconsider u9 = u as Element of ( Funcs (X,the carrier of Y));

        reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

        reconsider w = (( FuncExtMult (X,Y)) . [mj, u9]) as VECTOR of IT;

        take w;

        thus thesis by Th6;

      end;

      

       A3: for a be Complex, u,v be VECTOR of IT holds (a * (u + v)) = ((a * u) + (a * v))

      proof

        let a be Complex;

        let u,v be VECTOR of IT;

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

        (a * (u + v)) = ((a * u) + (a * v))

        proof

          reconsider v9 = v, u9 = u as Element of ( Funcs (X,the carrier of Y));

          reconsider w = (( FuncExtMult (X,Y)) . [a, u9]), w9 = (( FuncExtMult (X,Y)) . [a, v9]) as VECTOR of IT;

          (a * (u + v)) = (( FuncExtMult (X,Y)) . [a, (( FuncAdd (X,Y)) . (u9,v9))]) by CLVECT_1:def 1

          .= (( FuncAdd (X,Y)) . (w,w9)) by Lm1

          .= (w + (a * v)) by CLVECT_1:def 1

          .= ((a * u) + (a * v)) by CLVECT_1:def 1;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A4: for a,b be Complex, v be VECTOR of IT holds ((a * b) * v) = (a * (b * v))

      proof

        let a,b be Complex;

        let v be VECTOR of IT;

        reconsider v9 = v as Element of ( Funcs (X,the carrier of Y));

        

        thus ((a * b) * v) = (( FuncExtMult (X,Y)) . [(a * b), v9]) by CLVECT_1:def 1

        .= (( FuncExtMult (X,Y)) . [a, (( FuncExtMult (X,Y)) . [b, v9])]) by Th8

        .= (( FuncExtMult (X,Y)) . [a, (b * v)]) by CLVECT_1:def 1

        .= (a * (b * v)) by CLVECT_1:def 1;

      end;

      

       A5: for a,b be Complex, v be VECTOR of IT holds ((a + b) * v) = ((a * v) + (b * v))

      proof

        let a,b be Complex;

        let v be VECTOR of IT;

        reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;

        reconsider v9 = v as Element of ( Funcs (X,the carrier of Y));

        reconsider w = (( FuncExtMult (X,Y)) . [a, v9]), w9 = (( FuncExtMult (X,Y)) . [b, v9]) as VECTOR of IT;

        ((a + b) * v) = (( FuncExtMult (X,Y)) . [(a + b), v9]) by CLVECT_1:def 1

        .= (( FuncAdd (X,Y)) . (w,w9)) by Th9

        .= (w + (b * v)) by CLVECT_1:def 1

        .= ((a * v) + (b * v)) by CLVECT_1:def 1;

        hence thesis;

      end;

      

       A6: (u + ( 0. IT)) = u

      proof

        reconsider u9 = u as Element of ( Funcs (X,the carrier of Y));

        

        thus (u + ( 0. IT)) = (( FuncAdd (X,Y)) . (( FuncZero (X,Y)),u9)) by Th3

        .= u by Th5;

      end;

      

       A7: for v be VECTOR of IT holds ( 1r * v) = v

      proof

        let v be VECTOR of IT;

        reconsider v9 = v as Element of ( Funcs (X,the carrier of Y));

        

        thus ( 1r * v) = (( FuncExtMult (X,Y)) . [ 1r , v9]) by CLVECT_1:def 1

        .= v by Th7;

      end;

      (u + v) = (v + u) by Th3;

      hence thesis by A1, A6, A2, A3, A5, A4, A7, ALGSTR_0:def 16, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

    end;

    definition

      let X be non empty set;

      let Y be ComplexLinearSpace;

      :: CLOPBAN1:def2

      func ComplexVectSpace (X,Y) -> ComplexLinearSpace equals CLSStruct (# ( Funcs (X,the carrier of Y)), ( FuncZero (X,Y)), ( FuncAdd (X,Y)), ( FuncExtMult (X,Y)) #);

      coherence by Th10;

    end

    registration

      let X be non empty set;

      let Y be ComplexLinearSpace;

      cluster ( ComplexVectSpace (X,Y)) -> strict;

      coherence ;

    end

    registration

      let X be non empty set;

      let Y be ComplexLinearSpace;

      cluster ( ComplexVectSpace (X,Y)) -> constituted-Functions;

      coherence by MONOID_0: 80;

    end

    definition

      let X be non empty set;

      let Y be ComplexLinearSpace;

      let f be VECTOR of ( ComplexVectSpace (X,Y));

      let x be Element of X;

      :: original: .

      redefine

      func f . x -> VECTOR of Y ;

      coherence

      proof

        consider g be Function such that

         A1: f = g and

         A2: ( dom g) = X and

         A3: ( rng g) c= the carrier of Y by FUNCT_2:def 2;

        (f . x) in ( rng g) by A1, A2, FUNCT_1:def 3;

        hence thesis by A3;

      end;

    end

    theorem :: CLOPBAN1:11

    for X be non empty set, Y be ComplexLinearSpace, f,g,h be VECTOR of ( ComplexVectSpace (X,Y)) holds h = (f + g) iff for x be Element of X holds (h . x) = ((f . x) + (g . x)) by LOPBAN_1: 1;

    theorem :: CLOPBAN1:12

    

     Th12: for X be non empty set, Y be ComplexLinearSpace, f,h be VECTOR of ( ComplexVectSpace (X,Y)), c be Complex holds h = (c * f) iff for x be Element of X holds (h . x) = (c * (f . x))

    proof

      let X be non empty set;

      let Y be ComplexLinearSpace;

      let f,h be VECTOR of ( ComplexVectSpace (X,Y));

      let c be Complex;

      reconsider f9 = f, h9 = h as Element of ( Funcs (X,the carrier of Y));

      hereby

        assume

         A1: h = (c * f);

        let x be Element of X;

        h = (( FuncExtMult (X,Y)) . [c, f9]) by A1, CLVECT_1:def 1;

        hence (h . x) = (c * (f . x)) by Th2;

      end;

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

      then h9 = (( FuncExtMult (X,Y)) . [c, f9]) by Th2;

      hence thesis by CLVECT_1:def 1;

    end;

    begin

    definition

      let X,Y be non empty CLSStruct;

      let IT be Function of X, Y;

      :: CLOPBAN1:def3

      attr IT is homogeneous means

      : Def3: for x be VECTOR of X, r be Complex holds (IT . (r * x)) = (r * (IT . x));

    end

    registration

      let X be non empty CLSStruct;

      let Y be ComplexLinearSpace;

      cluster additive homogeneous for Function of X, Y;

      existence

      proof

        set f = (the carrier of X --> ( 0. Y));

        reconsider f as Function of X, Y;

        take f;

        hereby

          let x,y be VECTOR of X;

          

          thus (f . (x + y)) = ( 0. Y) by FUNCOP_1: 7

          .= (( 0. Y) + ( 0. Y)) by RLVECT_1: 4

          .= ((f . x) + ( 0. Y)) by FUNCOP_1: 7

          .= ((f . x) + (f . y)) by FUNCOP_1: 7;

        end;

        hereby

          let x be VECTOR of X, c be Complex;

          

          thus (f . (c * x)) = ( 0. Y) by FUNCOP_1: 7

          .= (c * ( 0. Y)) by CLVECT_1: 1

          .= (c * (f . x)) by FUNCOP_1: 7;

        end;

      end;

    end

    definition

      let X,Y be ComplexLinearSpace;

      mode LinearOperator of X,Y is additive homogeneous Function of X, Y;

    end

    definition

      let X,Y be ComplexLinearSpace;

      :: CLOPBAN1:def4

      func LinearOperators (X,Y) -> Subset of ( ComplexVectSpace (the carrier of X,Y)) means

      : Def4: for x be set holds x in it iff x is LinearOperator of X, Y;

      existence

      proof

        defpred P[ object] means $1 is LinearOperator of X, Y;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( Funcs (the carrier of X,the carrier of Y)) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( Funcs (the carrier of X,the carrier of Y)) by A1;

        hence IT is Subset of ( ComplexVectSpace (the carrier of X,Y)) by TARSKI:def 3;

        let x be set;

        thus x in IT implies x is LinearOperator of X, Y by A1;

        assume

         A2: x is LinearOperator of X, Y;

        then x in ( Funcs (the carrier of X,the carrier of Y)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( ComplexVectSpace (the carrier of X,Y));

        assume that

         A3: for x be set holds x in X1 iff x is LinearOperator of X, Y and

         A4: for x be set holds x in X2 iff x is LinearOperator of X, Y;

        for x be object st x in X2 holds x in X1

        proof

          let x be object;

          assume x in X2;

          then x is LinearOperator of X, Y by A4;

          hence thesis by A3;

        end;

        then

         A5: X2 c= X1 by TARSKI:def 3;

        for x be object st x in X1 holds x in X2

        proof

          let x be object;

          assume x in X1;

          then x is LinearOperator of X, Y by A3;

          hence thesis by A4;

        end;

        then X1 c= X2 by TARSKI:def 3;

        hence thesis by A5, XBOOLE_0:def 10;

      end;

    end

    registration

      let X,Y be ComplexLinearSpace;

      cluster ( LinearOperators (X,Y)) -> non empty functional;

      coherence

      proof

        set f = (the carrier of X --> ( 0. Y));

        

         A1: f is homogeneous

        proof

          let x be VECTOR of X, c be Complex;

          

          thus (f . (c * x)) = ( 0. Y) by FUNCOP_1: 7

          .= (c * ( 0. Y)) by CLVECT_1: 1

          .= (c * (f . x)) by FUNCOP_1: 7;

        end;

        f is additive

        proof

          let x,y be VECTOR of X;

          

          thus (f . (x + y)) = ( 0. Y) by FUNCOP_1: 7

          .= (( 0. Y) + ( 0. Y)) by RLVECT_1: 4

          .= ((f . x) + ( 0. Y)) by FUNCOP_1: 7

          .= ((f . x) + (f . y)) by FUNCOP_1: 7;

        end;

        hence ( LinearOperators (X,Y)) is non empty by A1, Def4;

        let x be object;

        thus thesis;

      end;

    end

    theorem :: CLOPBAN1:13

    

     Th13: for X,Y be ComplexLinearSpace holds ( LinearOperators (X,Y)) is linearly-closed

    proof

      let X,Y be ComplexLinearSpace;

      set W = ( LinearOperators (X,Y));

      

       A1: for c be Complex holds for v be VECTOR of ( ComplexVectSpace (the carrier of X,Y)) st v in W holds (c * v) in W

      proof

        let c be Complex;

        let v be VECTOR of ( ComplexVectSpace (the carrier of X,Y)) such that

         A2: v in W;

        (c * v) is LinearOperator of X, Y

        proof

          reconsider f = (c * v) as Function of X, Y by FUNCT_2: 66;

          

           A3: f is homogeneous

          proof

            reconsider v9 = v as Element of ( Funcs (the carrier of X,the carrier of Y));

            let x be VECTOR of X, s be Complex;

            

             A4: v9 is LinearOperator of X, Y by A2, Def4;

            

             A5: f = (( FuncExtMult (the carrier of X,Y)) . [c, v9]) by CLVECT_1:def 1;

            

            hence (f . (s * x)) = (c * (v9 . (s * x))) by Th2

            .= (c * (s * (v9 . x))) by A4, Def3

            .= ((c * s) * (v9 . x)) by CLVECT_1:def 4

            .= (s * (c * (v9 . x))) by CLVECT_1:def 4

            .= (s * (f . x)) by A5, Th2;

          end;

          f is additive

          proof

            reconsider v9 = v as Element of ( Funcs (the carrier of X,the carrier of Y));

            let x,y be VECTOR of X;

            

             A6: v9 is LinearOperator of X, Y by A2, Def4;

            

             A7: f = (( FuncExtMult (the carrier of X,Y)) . [c, v9]) by CLVECT_1:def 1;

            

            hence (f . (x + y)) = (c * (v9 . (x + y))) by Th2

            .= (c * ((v9 . x) + (v9 . y))) by A6, VECTSP_1:def 20

            .= ((c * (v9 . x)) + (c * (v9 . y))) by CLVECT_1:def 2

            .= ((f . x) + (c * (v9 . y))) by A7, Th2

            .= ((f . x) + (f . y)) by A7, Th2;

          end;

          hence thesis by A3;

        end;

        hence thesis by Def4;

      end;

      for v,u be VECTOR of ( ComplexVectSpace (the carrier of X,Y)) st v in ( LinearOperators (X,Y)) & u in ( LinearOperators (X,Y)) holds (v + u) in ( LinearOperators (X,Y))

      proof

        let v,u be VECTOR of ( ComplexVectSpace (the carrier of X,Y)) such that

         A8: v in W and

         A9: u in W;

        (v + u) is LinearOperator of X, Y

        proof

          reconsider f = (v + u) as Function of X, Y by FUNCT_2: 66;

          

           A10: f is homogeneous

          proof

            reconsider v9 = v, u9 = u as Element of ( Funcs (the carrier of X,the carrier of Y));

            let x be VECTOR of X, s be Complex;

            

             A11: u9 is LinearOperator of X, Y by A9, Def4;

            

             A12: v9 is LinearOperator of X, Y by A8, Def4;

            

            thus (f . (s * x)) = ((u9 . (s * x)) + (v9 . (s * x))) by LOPBAN_1: 1

            .= ((s * (u9 . x)) + (v9 . (s * x))) by A11, Def3

            .= ((s * (u9 . x)) + (s * (v9 . x))) by A12, Def3

            .= (s * ((u9 . x) + (v9 . x))) by CLVECT_1:def 2

            .= (s * (f . x)) by LOPBAN_1: 1;

          end;

          f is additive

          proof

            reconsider v9 = v, u9 = u as Element of ( Funcs (the carrier of X,the carrier of Y));

            let x,y be VECTOR of X;

            

             A13: u9 is LinearOperator of X, Y by A9, Def4;

            

             A14: v9 is LinearOperator of X, Y by A8, Def4;

            

            thus (f . (x + y)) = ((u9 . (x + y)) + (v9 . (x + y))) by LOPBAN_1: 1

            .= (((u9 . x) + (u9 . y)) + (v9 . (x + y))) by A13, VECTSP_1:def 20

            .= (((u9 . x) + (u9 . y)) + ((v9 . x) + (v9 . y))) by A14, VECTSP_1:def 20

            .= ((((u9 . x) + (u9 . y)) + (v9 . x)) + (v9 . y)) by RLVECT_1:def 3

            .= ((((u9 . x) + (v9 . x)) + (u9 . y)) + (v9 . y)) by RLVECT_1:def 3

            .= (((f . x) + (u9 . y)) + (v9 . y)) by LOPBAN_1: 1

            .= ((f . x) + ((u9 . y) + (v9 . y))) by RLVECT_1:def 3

            .= ((f . x) + (f . y)) by LOPBAN_1: 1;

          end;

          hence thesis by A10;

        end;

        hence thesis by Def4;

      end;

      hence thesis by A1, CLVECT_1:def 7;

    end;

    theorem :: CLOPBAN1:14

    for X,Y be ComplexLinearSpace holds CLSStruct (# ( LinearOperators (X,Y)), ( Zero_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))), ( Add_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))), ( Mult_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))) #) is Subspace of ( ComplexVectSpace (the carrier of X,Y)) by Th13, CSSPACE: 11;

    registration

      let X,Y be ComplexLinearSpace;

      cluster CLSStruct (# ( LinearOperators (X,Y)), ( Zero_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))), ( Add_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))), ( Mult_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th13, CSSPACE: 11;

    end

    definition

      let X,Y be ComplexLinearSpace;

      :: CLOPBAN1:def5

      func C_VectorSpace_of_LinearOperators (X,Y) -> ComplexLinearSpace equals CLSStruct (# ( LinearOperators (X,Y)), ( Zero_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))), ( Add_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))), ( Mult_ (( LinearOperators (X,Y)),( ComplexVectSpace (the carrier of X,Y)))) #);

      coherence ;

    end

    registration

      let X,Y be ComplexLinearSpace;

      cluster ( C_VectorSpace_of_LinearOperators (X,Y)) -> strict;

      coherence ;

    end

    registration

      let X,Y be ComplexLinearSpace;

      cluster ( C_VectorSpace_of_LinearOperators (X,Y)) -> constituted-Functions;

      coherence by MONOID_0: 80;

    end

    definition

      let X,Y be ComplexLinearSpace;

      let f be Element of ( C_VectorSpace_of_LinearOperators (X,Y));

      let v be VECTOR of X;

      :: original: .

      redefine

      func f . v -> VECTOR of Y ;

      coherence

      proof

        reconsider f as LinearOperator of X, Y by Def4;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: CLOPBAN1:15

    

     Th15: for X,Y be ComplexLinearSpace, f,g,h be VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) holds h = (f + g) iff for x be VECTOR of X holds (h . x) = ((f . x) + (g . x))

    proof

      let X,Y be ComplexLinearSpace;

      let f,g,h be VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y));

      reconsider f9 = f, g9 = g, h9 = h as LinearOperator of X, Y by Def4;

      

       A1: ( C_VectorSpace_of_LinearOperators (X,Y)) is Subspace of ( ComplexVectSpace (the carrier of X,Y)) by Th13, CSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( ComplexVectSpace (the carrier of X,Y)) by CLVECT_1: 29;

      reconsider h1 = h as VECTOR of ( ComplexVectSpace (the carrier of X,Y)) by A1, CLVECT_1: 29;

      reconsider g1 = g as VECTOR of ( ComplexVectSpace (the carrier of X,Y)) by A1, CLVECT_1: 29;

       A2:

      now

        assume

         A3: h = (f + g);

        let x be Element of X;

        h1 = (f1 + g1) by A1, A3, CLVECT_1: 32;

        hence (h9 . x) = ((f9 . x) + (g9 . x)) by LOPBAN_1: 1;

      end;

      now

        assume for x be Element of X holds (h9 . x) = ((f9 . x) + (g9 . x));

        then h1 = (f1 + g1) by LOPBAN_1: 1;

        hence h = (f + g) by A1, CLVECT_1: 32;

      end;

      hence thesis by A2;

    end;

    theorem :: CLOPBAN1:16

    

     Th16: for X,Y be ComplexLinearSpace, f,h be VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)), c be Complex holds h = (c * f) iff for x be VECTOR of X holds (h . x) = (c * (f . x))

    proof

      let X,Y be ComplexLinearSpace;

      let f,h be VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y));

      reconsider f9 = f, h9 = h as LinearOperator of X, Y by Def4;

      let c be Complex;

      

       A1: ( C_VectorSpace_of_LinearOperators (X,Y)) is Subspace of ( ComplexVectSpace (the carrier of X,Y)) by Th13, CSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( ComplexVectSpace (the carrier of X,Y)) by CLVECT_1: 29;

      reconsider h1 = h as VECTOR of ( ComplexVectSpace (the carrier of X,Y)) by A1, CLVECT_1: 29;

       A2:

      now

        assume

         A3: h = (c * f);

        let x be Element of X;

        h1 = (c * f1) by A1, A3, CLVECT_1: 33;

        hence (h9 . x) = (c * (f9 . x)) by Th12;

      end;

      now

        assume for x be Element of X holds (h9 . x) = (c * (f9 . x));

        then h1 = (c * f1) by Th12;

        hence h = (c * f) by A1, CLVECT_1: 33;

      end;

      hence thesis by A2;

    end;

    theorem :: CLOPBAN1:17

    

     Th17: for X,Y be ComplexLinearSpace holds ( 0. ( C_VectorSpace_of_LinearOperators (X,Y))) = (the carrier of X --> ( 0. Y))

    proof

      let X,Y be ComplexLinearSpace;

      

       A1: ( 0. ( ComplexVectSpace (the carrier of X,Y))) = (the carrier of X --> ( 0. Y)) by LOPBAN_1:def 3;

      ( C_VectorSpace_of_LinearOperators (X,Y)) is Subspace of ( ComplexVectSpace (the carrier of X,Y)) by Th13, CSSPACE: 11;

      hence thesis by A1, CLVECT_1: 30;

    end;

    theorem :: CLOPBAN1:18

    

     Th18: for X,Y be ComplexLinearSpace holds (the carrier of X --> ( 0. Y)) is LinearOperator of X, Y

    proof

      let X,Y be ComplexLinearSpace;

      set f = (the carrier of X --> ( 0. Y));

      reconsider f as Function of X, Y;

      

       A1: f is homogeneous

      proof

        let x be VECTOR of X, c be Complex;

        

        thus (f . (c * x)) = ( 0. Y) by FUNCOP_1: 7

        .= (c * ( 0. Y)) by CLVECT_1: 1

        .= (c * (f . x)) by FUNCOP_1: 7;

      end;

      f is additive

      proof

        let x,y be VECTOR of X;

        

        thus (f . (x + y)) = ( 0. Y) by FUNCOP_1: 7

        .= (( 0. Y) + ( 0. Y)) by RLVECT_1: 4

        .= ((f . x) + ( 0. Y)) by FUNCOP_1: 7

        .= ((f . x) + (f . y)) by FUNCOP_1: 7;

      end;

      hence thesis by A1;

    end;

    begin

    theorem :: CLOPBAN1:19

    

     Th19: for X be ComplexNormSpace, seq be sequence of X, g be Point of X holds seq is convergent & ( lim seq) = g implies ||.seq.|| is convergent & ( lim ||.seq.||) = ||.g.||

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let g be Point of X;

      assume that

       A1: seq is convergent and

       A2: ( lim seq) = g;

       A3:

      now

        let r be Real;

        assume

         A4: r > 0 ;

        consider m1 be Nat such that

         A5: for n be Nat st n >= m1 holds ||.((seq . n) - g).|| < r by A1, A2, A4, CLVECT_1:def 16;

        take k = m1;

        now

          let n be Nat;

          assume n >= k;

          then

           A6: ||.((seq . n) - g).|| < r by A5;

           |.( ||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by CLVECT_1: 110;

          then |.( ||.(seq . n).|| - ||.g.||).| < r by A6, XXREAL_0: 2;

          hence |.(( ||.seq.|| . n) - ||.g.||).| < r by NORMSP_0:def 4;

        end;

        hence for n be Nat st k <= n holds |.(( ||.seq.|| . n) - ||.g.||).| < r;

      end;

       ||.seq.|| is convergent by A1, CLVECT_1: 117;

      hence thesis by A3, SEQ_2:def 7;

    end;

    definition

      let X,Y be ComplexNormSpace;

      let IT be LinearOperator of X, Y;

      :: CLOPBAN1:def6

      attr IT is Lipschitzian means

      : Def6: ex K be Real st 0 <= K & for x be VECTOR of X holds ||.(IT . x).|| <= (K * ||.x.||);

    end

    theorem :: CLOPBAN1:20

    

     Th20: for X,Y be ComplexNormSpace holds for f be LinearOperator of X, Y st (for x be VECTOR of X holds (f . x) = ( 0. Y)) holds f is Lipschitzian

    proof

      let X,Y be ComplexNormSpace;

      let f be LinearOperator of X, Y such that

       A1: for x be VECTOR of X holds (f . x) = ( 0. Y);

       A2:

      now

        let x be VECTOR of X;

        

        thus ||.(f . x).|| = ||.( 0. Y).|| by A1

        .= ( 0 * ||.x.||) by CLVECT_1: 102;

      end;

      take 0 ;

      thus thesis by A2;

    end;

    registration

      let X,Y be ComplexNormSpace;

      cluster Lipschitzian for LinearOperator of X, Y;

      existence

      proof

        set f = (the carrier of X --> ( 0. Y));

        reconsider f as LinearOperator of X, Y by Th18;

        take f;

        for x be VECTOR of X holds (f . x) = ( 0. Y) by FUNCOP_1: 7;

        hence thesis by Th20;

      end;

    end

    definition

      let X,Y be ComplexNormSpace;

      :: CLOPBAN1:def7

      func BoundedLinearOperators (X,Y) -> Subset of ( C_VectorSpace_of_LinearOperators (X,Y)) means

      : Def7: for x be set holds x in it iff x is Lipschitzian LinearOperator of X, Y;

      existence

      proof

        defpred P[ object] means $1 is Lipschitzian LinearOperator of X, Y;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( LinearOperators (X,Y)) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( LinearOperators (X,Y)) by A1;

        hence IT is Subset of ( C_VectorSpace_of_LinearOperators (X,Y)) by TARSKI:def 3;

        let x be set;

        thus x in IT implies x is Lipschitzian LinearOperator of X, Y by A1;

        assume

         A2: x is Lipschitzian LinearOperator of X, Y;

        then x in ( LinearOperators (X,Y)) by Def4;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( C_VectorSpace_of_LinearOperators (X,Y));

        assume that

         A3: for x be set holds x in X1 iff x is Lipschitzian LinearOperator of X, Y and

         A4: for x be set holds x in X2 iff x is Lipschitzian LinearOperator of X, Y;

        for x be object st x in X2 holds x in X1

        proof

          let x be object;

          assume x in X2;

          then x is Lipschitzian LinearOperator of X, Y by A4;

          hence thesis by A3;

        end;

        then

         A5: X2 c= X1 by TARSKI:def 3;

        for x be object st x in X1 holds x in X2

        proof

          let x be object;

          assume x in X1;

          then x is Lipschitzian LinearOperator of X, Y by A3;

          hence thesis by A4;

        end;

        then X1 c= X2 by TARSKI:def 3;

        hence thesis by A5, XBOOLE_0:def 10;

      end;

    end

    registration

      let X,Y be ComplexNormSpace;

      cluster ( BoundedLinearOperators (X,Y)) -> non empty;

      coherence

      proof

        set f = (the carrier of X --> ( 0. Y));

        reconsider f as LinearOperator of X, Y by Th18;

        for x be VECTOR of X holds (f . x) = ( 0. Y) by FUNCOP_1: 7;

        then f is Lipschitzian by Th20;

        hence thesis by Def7;

      end;

    end

    theorem :: CLOPBAN1:21

    

     Th21: for X,Y be ComplexNormSpace holds ( BoundedLinearOperators (X,Y)) is linearly-closed

    proof

      let X,Y be ComplexNormSpace;

      set W = ( BoundedLinearOperators (X,Y));

      

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

      proof

        let v,u be VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) such that

         A2: v in W and

         A3: u in W;

        reconsider f = (v + u) as LinearOperator of X, Y by Def4;

        f is Lipschitzian

        proof

          reconsider v1 = v as Lipschitzian LinearOperator of X, Y by A2, Def7;

          consider K2 be Real such that

           A4: 0 <= K2 and

           A5: for x be VECTOR of X holds ||.(v1 . x).|| <= (K2 * ||.x.||) by Def6;

          reconsider u1 = u as Lipschitzian LinearOperator of X, Y by A3, Def7;

          consider K1 be Real such that

           A6: 0 <= K1 and

           A7: for x be VECTOR of X holds ||.(u1 . x).|| <= (K1 * ||.x.||) by Def6;

          take K3 = (K1 + K2);

          now

            let x be VECTOR of X;

            

             A8: ||.((u1 . x) + (v1 . x)).|| <= ( ||.(u1 . x).|| + ||.(v1 . x).||) by CLVECT_1:def 13;

            

             A9: ||.(v1 . x).|| <= (K2 * ||.x.||) by A5;

             ||.(u1 . x).|| <= (K1 * ||.x.||) by A7;

            then

             A10: ( ||.(u1 . x).|| + ||.(v1 . x).||) <= ((K1 * ||.x.||) + (K2 * ||.x.||)) by A9, XREAL_1: 7;

             ||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th15;

            hence ||.(f . x).|| <= (K3 * ||.x.||) by A8, A10, XXREAL_0: 2;

          end;

          hence thesis by A6, A4;

        end;

        hence thesis by Def7;

      end;

      for c be Complex, v be VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) st v in W holds (c * v) in W

      proof

        let c be Complex;

        let v be VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) such that

         A11: v in W;

        reconsider f = (c * v) as LinearOperator of X, Y by Def4;

        f is Lipschitzian

        proof

          reconsider v1 = v as Lipschitzian LinearOperator of X, Y by A11, Def7;

          consider K be Real such that

           A12: 0 <= K and

           A13: for x be VECTOR of X holds ||.(v1 . x).|| <= (K * ||.x.||) by Def6;

          take ( |.c.| * K);

           A14:

          now

            let x be VECTOR of X;

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

            then

             A15: ( |.c.| * ||.(v1 . x).||) <= ( |.c.| * (K * ||.x.||)) by A13, XREAL_1: 64;

             ||.(c * (v1 . x)).|| = ( |.c.| * ||.(v1 . x).||) by CLVECT_1:def 13;

            hence ||.(f . x).|| <= (( |.c.| * K) * ||.x.||) by A15, Th16;

          end;

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

          hence thesis by A12, A14;

        end;

        hence thesis by Def7;

      end;

      hence thesis by A1, CLVECT_1:def 7;

    end;

    theorem :: CLOPBAN1:22

    for X,Y be ComplexNormSpace holds CLSStruct (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))) #) is Subspace of ( C_VectorSpace_of_LinearOperators (X,Y)) by Th21, CSSPACE: 11;

    registration

      let X,Y be ComplexNormSpace;

      cluster CLSStruct (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th21, CSSPACE: 11;

    end

    definition

      let X,Y be ComplexNormSpace;

      :: CLOPBAN1:def8

      func C_VectorSpace_of_BoundedLinearOperators (X,Y) -> ComplexLinearSpace equals CLSStruct (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))) #);

      coherence ;

    end

    registration

      let X,Y be ComplexNormSpace;

      cluster ( C_VectorSpace_of_BoundedLinearOperators (X,Y)) -> strict;

      coherence ;

    end

    registration

      let X,Y be ComplexNormSpace;

      cluster -> Function-like Relation-like for Element of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

      coherence ;

    end

    definition

      let X,Y be ComplexNormSpace;

      let f be Element of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

      let v be VECTOR of X;

      :: original: .

      redefine

      func f . v -> VECTOR of Y ;

      coherence

      proof

        reconsider f as LinearOperator of X, Y by Def7;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: CLOPBAN1:23

    

     Th23: for X,Y be ComplexNormSpace, f,g,h be VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y)) holds h = (f + g) iff for x be VECTOR of X holds (h . x) = ((f . x) + (g . x))

    proof

      let X,Y be ComplexNormSpace;

      let f,g,h be VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

      

       A1: ( C_VectorSpace_of_BoundedLinearOperators (X,Y)) is Subspace of ( C_VectorSpace_of_LinearOperators (X,Y)) by Th21, CSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) by CLVECT_1: 29;

      reconsider h1 = h as VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) by A1, CLVECT_1: 29;

      reconsider g1 = g as VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) by A1, CLVECT_1: 29;

      hereby

        assume

         A2: h = (f + g);

        let x be Element of X;

        h1 = (f1 + g1) by A1, A2, CLVECT_1: 32;

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

      end;

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

      then h1 = (f1 + g1) by Th15;

      hence thesis by A1, CLVECT_1: 32;

    end;

    theorem :: CLOPBAN1:24

    

     Th24: for X,Y be ComplexNormSpace, f,h be VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y)), c be Complex holds h = (c * f) iff for x be VECTOR of X holds (h . x) = (c * (f . x))

    proof

      let X,Y be ComplexNormSpace;

      let f,h be VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

      let c be Complex;

      

       A1: ( C_VectorSpace_of_BoundedLinearOperators (X,Y)) is Subspace of ( C_VectorSpace_of_LinearOperators (X,Y)) by Th21, CSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) by CLVECT_1: 29;

      reconsider h1 = h as VECTOR of ( C_VectorSpace_of_LinearOperators (X,Y)) by A1, CLVECT_1: 29;

      hereby

        assume

         A2: h = (c * f);

        let x be Element of X;

        h1 = (c * f1) by A1, A2, CLVECT_1: 33;

        hence (h . x) = (c * (f . x)) by Th16;

      end;

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

      then h1 = (c * f1) by Th16;

      hence thesis by A1, CLVECT_1: 33;

    end;

    theorem :: CLOPBAN1:25

    

     Th25: for X,Y be ComplexNormSpace holds ( 0. ( C_VectorSpace_of_BoundedLinearOperators (X,Y))) = (the carrier of X --> ( 0. Y))

    proof

      let X,Y be ComplexNormSpace;

      

       A1: ( 0. ( C_VectorSpace_of_LinearOperators (X,Y))) = (the carrier of X --> ( 0. Y)) by Th17;

      ( C_VectorSpace_of_BoundedLinearOperators (X,Y)) is Subspace of ( C_VectorSpace_of_LinearOperators (X,Y)) by Th21, CSSPACE: 11;

      hence thesis by A1, CLVECT_1: 30;

    end;

    definition

      let X,Y be ComplexNormSpace;

      let f be object;

      :: CLOPBAN1:def9

      func modetrans (f,X,Y) -> Lipschitzian LinearOperator of X, Y equals

      : Def9: f;

      coherence by A1, Def7;

    end

    definition

      let X,Y be ComplexNormSpace;

      let u be LinearOperator of X, Y;

      :: CLOPBAN1:def10

      func PreNorms (u) -> non empty Subset of REAL equals { ||.(u . t).|| where t be VECTOR of X : ||.t.|| <= 1 };

      coherence

      proof

         A1:

        now

          let x be object;

          now

            assume x in { ||.(u . t).|| where t be VECTOR of X : ||.t.|| <= 1 };

            then ex t be VECTOR of X st x = ||.(u . t).|| & ||.t.|| <= 1;

            hence x in REAL ;

          end;

          hence x in { ||.(u . t).|| where t be VECTOR of X : ||.t.|| <= 1 } implies x in REAL ;

        end;

         ||.( 0. X).|| = 0 by CLVECT_1: 102;

        then ||.(u . ( 0. X)).|| in { ||.(u . t).|| where t be VECTOR of X : ||.t.|| <= 1 };

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: CLOPBAN1:26

    

     Th26: for X,Y be ComplexNormSpace, g be Lipschitzian LinearOperator of X, Y holds ( PreNorms g) is bounded_above

    proof

      let X,Y be ComplexNormSpace;

      let g be Lipschitzian LinearOperator of X, Y;

      ( PreNorms g) is bounded_above

      proof

        consider K be Real such that

         A1: 0 <= K and

         A2: for x be VECTOR of X holds ||.(g . x).|| <= (K * ||.x.||) by Def6;

        take K;

        let r be ExtReal;

        assume r in ( PreNorms g);

        then

        consider t be VECTOR of X such that

         A3: r = ||.(g . t).|| and

         A4: ||.t.|| <= 1;

        

         A5: ||.(g . t).|| <= (K * ||.t.||) by A2;

        (K * ||.t.||) <= (K * 1) by A1, A4, XREAL_1: 64;

        hence r <= K by A3, A5, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: CLOPBAN1:27

    for X,Y be ComplexNormSpace, g be LinearOperator of X, Y holds g is Lipschitzian iff ( PreNorms g) is bounded_above

    proof

      let X,Y be ComplexNormSpace;

      let g be LinearOperator of X, Y;

      now

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

        assume

         A1: ( PreNorms g) is bounded_above;

         A2:

        now

          let t be VECTOR of X;

          now

            per cases ;

              case

               A3: t = ( 0. X);

              then

               A4: ||.t.|| = 0 by NORMSP_0:def 6;

              (g . t) = (g . ( 0c * ( 0. X))) by A3, CLVECT_1: 1

              .= ( 0c * (g . ( 0. X))) by Def3

              .= ( 0. Y) by CLVECT_1: 1;

              hence ||.(g . t).|| <= (K * ||.t.||) by A4, NORMSP_0:def 6;

            end;

              case

               A5: t <> ( 0. X);

              reconsider t0 = (( ||.t.|| " ) + ( 0 * <i> )) as Element of COMPLEX by XCMPLX_0:def 2;

              reconsider t1 = (t0 * t) as VECTOR of X;

              

               A6: ||.t.|| <> 0 by A5, NORMSP_0:def 5;

              then

               A7: ||.t.|| > 0 by CLVECT_1: 105;

              

               A8: |.(( ||.t.|| " ) + ( 0 * <i> )).| = |.(1 * ( ||.t.|| " )).|

              .= |.(1 / ||.t.||).| by XCMPLX_0:def 9

              .= (1 / |. ||.t.||.|) by ABSVALUE: 7

              .= (1 / ||.t.||) by A7, ABSVALUE:def 1

              .= (1 * ( ||.t.|| " )) by XCMPLX_0:def 9

              .= ( ||.t.|| " );

              

              then

               A9: ( ||.(g . t).|| / ||.t.||) = ( ||.(g . t).|| * |.t0.|) by XCMPLX_0:def 9

              .= ||.(t0 * (g . t)).|| by CLVECT_1:def 13

              .= ||.(g . t1).|| by Def3;

               ||.t1.|| = ( |.t0.| * ||.t.||) by CLVECT_1:def 13

              .= 1 by A6, A8, XCMPLX_0:def 7;

              then ( ||.(g . t).|| / ||.t.||) in ( PreNorms g) by A9;

              then

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

              (( ||.(g . t).|| / ||.t.||) * ||.t.||) = (( ||.(g . t).|| * ( ||.t.|| " )) * ||.t.||) by XCMPLX_0:def 9

              .= ( ||.(g . t).|| * (( ||.t.|| " ) * ||.t.||))

              .= ( ||.(g . t).|| * 1) by A6, XCMPLX_0:def 7

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

              hence ||.(g . t).|| <= (K * ||.t.||) by A7, A10, XREAL_1: 64;

            end;

          end;

          hence ||.(g . t).|| <= (K * ||.t.||);

        end;

        take K;

         0 <= K

        proof

          consider r0 be object such that

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

          reconsider r0 as Real by A11;

          now

            let r be Real;

            assume r in ( PreNorms g);

            then ex t be VECTOR of X st r = ||.(g . t).|| & ||.t.|| <= 1;

            hence 0 <= r by CLVECT_1: 105;

          end;

          then 0 <= r0 by A11;

          hence thesis by A1, A11, SEQ_4:def 1;

        end;

        hence g is Lipschitzian by A2;

      end;

      hence thesis by Th26;

    end;

    definition

      let X,Y be ComplexNormSpace;

      :: CLOPBAN1:def11

      func BoundedLinearOperatorsNorm (X,Y) -> Function of ( BoundedLinearOperators (X,Y)), REAL means

      : Def11: for x be object st x in ( BoundedLinearOperators (X,Y)) holds (it . x) = ( upper_bound ( PreNorms ( modetrans (x,X,Y))));

      existence

      proof

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

        

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

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

        hence thesis;

      end;

      uniqueness

      proof

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

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

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

        

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

        proof

          let z be object such that

           A5: z in ( BoundedLinearOperators (X,Y));

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

          hence thesis by A3, A5;

        end;

        

         A6: ( dom NORM2) = ( BoundedLinearOperators (X,Y)) by FUNCT_2:def 1;

        ( dom NORM1) = ( BoundedLinearOperators (X,Y)) by FUNCT_2:def 1;

        hence thesis by A6, A4;

      end;

    end

    theorem :: CLOPBAN1:28

    

     Th28: for X,Y be ComplexNormSpace, f be Lipschitzian LinearOperator of X, Y holds ( modetrans (f,X,Y)) = f

    proof

      let X,Y be ComplexNormSpace;

      let f be Lipschitzian LinearOperator of X, Y;

      f in ( BoundedLinearOperators (X,Y)) by Def7;

      hence thesis by Def9;

    end;

    theorem :: CLOPBAN1:29

    

     Th29: for X,Y be ComplexNormSpace, f be Lipschitzian LinearOperator of X, Y holds (( BoundedLinearOperatorsNorm (X,Y)) . f) = ( upper_bound ( PreNorms f))

    proof

      let X,Y be ComplexNormSpace;

      let f be Lipschitzian LinearOperator of X, Y;

      reconsider f9 = f as set;

      f in ( BoundedLinearOperators (X,Y)) by Def7;

      

      hence (( BoundedLinearOperatorsNorm (X,Y)) . f) = ( upper_bound ( PreNorms ( modetrans (f9,X,Y)))) by Def11

      .= ( upper_bound ( PreNorms f)) by Th28;

    end;

    definition

      let X,Y be ComplexNormSpace;

      :: CLOPBAN1:def12

      func C_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty CNORMSTR equals CNORMSTR (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( BoundedLinearOperatorsNorm (X,Y)) #);

      coherence ;

    end

    theorem :: CLOPBAN1:30

    

     Th30: for X,Y be ComplexNormSpace holds (the carrier of X --> ( 0. Y)) = ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)))

    proof

      let X,Y be ComplexNormSpace;

      (the carrier of X --> ( 0. Y)) = ( 0. ( C_VectorSpace_of_BoundedLinearOperators (X,Y))) by Th25

      .= ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)));

      hence thesis;

    end;

    theorem :: CLOPBAN1:31

    

     Th31: for X,Y be ComplexNormSpace, f be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)), g be Lipschitzian LinearOperator of X, Y st g = f holds for t be VECTOR of X holds ||.(g . t).|| <= ( ||.f.|| * ||.t.||)

    proof

      let X,Y be ComplexNormSpace;

      let f be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      let g be Lipschitzian LinearOperator of X, Y such that

       A1: g = f;

      

       A2: ( PreNorms g) is non empty bounded_above by Th26;

      now

        let t be VECTOR of X;

        now

          per cases ;

            case

             A3: t = ( 0. X);

            then

             A4: ||.t.|| = 0 by NORMSP_0:def 6;

            (g . t) = (g . ( 0c * ( 0. X))) by A3, CLVECT_1: 1

            .= ( 0c * (g . ( 0. X))) by Def3

            .= ( 0. Y) by CLVECT_1: 1;

            hence ||.(g . t).|| <= ( ||.f.|| * ||.t.||) by A4, NORMSP_0:def 6;

          end;

            case

             A5: t <> ( 0. X);

            reconsider t0 = (( ||.t.|| " ) + ( 0 * <i> )) as Element of COMPLEX by XCMPLX_0:def 2;

            reconsider t1 = (t0 * t) as VECTOR of X;

            

             A6: ||.t.|| <> 0 by A5, NORMSP_0:def 5;

            then

             A7: ||.t.|| > 0 by CLVECT_1: 105;

            

             A8: |.t0.| = |.(1 * ( ||.t.|| " )).|

            .= |.(1 / ||.t.||).| by XCMPLX_0:def 9

            .= (1 / |. ||.t.||.|) by ABSVALUE: 7

            .= (1 / ||.t.||) by A7, ABSVALUE:def 1

            .= (1 * ( ||.t.|| " )) by XCMPLX_0:def 9

            .= ( ||.t.|| " );

            

            then

             A9: ( ||.(g . t).|| / ||.t.||) = ( ||.(g . t).|| * |.t0.|) by XCMPLX_0:def 9

            .= ||.(t0 * (g . t)).|| by CLVECT_1:def 13

            .= ||.(g . t1).|| by Def3;

             ||.t1.|| = ( |.t0.| * ||.t.||) by CLVECT_1:def 13

            .= 1 by A6, A8, XCMPLX_0:def 7;

            then ( ||.(g . t).|| / ||.t.||) in { ||.(g . s).|| where s be VECTOR of X : ||.s.|| <= 1 } by A9;

            then ( ||.(g . t).|| / ||.t.||) <= ( upper_bound ( PreNorms g)) by A2, SEQ_4:def 1;

            then ( ||.(g . t).|| / ||.t.||) <= (( BoundedLinearOperatorsNorm (X,Y)) . g) by Th29;

            then

             A10: ( ||.(g . t).|| / ||.t.||) <= ||.f.|| by A1;

            (( ||.(g . t).|| / ||.t.||) * ||.t.||) = (( ||.(g . t).|| * ( ||.t.|| " )) * ||.t.||) by XCMPLX_0:def 9

            .= ( ||.(g . t).|| * (( ||.t.|| " ) * ||.t.||))

            .= ( ||.(g . t).|| * 1) by A6, XCMPLX_0:def 7

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

            hence ||.(g . t).|| <= ( ||.f.|| * ||.t.||) by A7, A10, XREAL_1: 64;

          end;

        end;

        hence ||.(g . t).|| <= ( ||.f.|| * ||.t.||);

      end;

      hence thesis;

    end;

    theorem :: CLOPBAN1:32

    

     Th32: for X,Y be ComplexNormSpace, f be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||

    proof

      let X,Y be ComplexNormSpace;

      let f be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      reconsider g = f as Lipschitzian LinearOperator of X, Y by Def7;

      consider r0 be object such that

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

      reconsider r0 as Real by A1;

      

       A2: ( PreNorms g) is non empty bounded_above by Th26;

      

       A3: (( BoundedLinearOperatorsNorm (X,Y)) . f) = ( upper_bound ( PreNorms g)) by Th29;

      now

        let r be Real;

        assume r in ( PreNorms g);

        then ex t be VECTOR of X st r = ||.(g . t).|| & ||.t.|| <= 1;

        hence 0 <= r by CLVECT_1: 105;

      end;

      then 0 <= r0 by A1;

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

      hence thesis by A3;

    end;

    theorem :: CLOPBAN1:33

    

     Th33: for X,Y be ComplexNormSpace, f be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) st f = ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y))) holds 0 = ||.f.||

    proof

      let X,Y be ComplexNormSpace;

      let f be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) such that

       A1: f = ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)));

      thus ||.f.|| = 0

      proof

        reconsider g = f as Lipschitzian LinearOperator of X, Y by Def7;

        set z = (the carrier of X --> ( 0. Y));

        reconsider z as Function of the carrier of X, the carrier of Y;

        consider r0 be object such that

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

        reconsider r0 as Real by A2;

        

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

        

         A4: ( PreNorms g) is non empty bounded_above by Th26;

        

         A5: z = g by A1, Th30;

         A6:

        now

          let r be Real;

          assume r in ( PreNorms g);

          then

          consider t be VECTOR of X such that

           A7: r = ||.(g . t).|| and ||.t.|| <= 1;

           ||.(g . t).|| = ||.( 0. Y).|| by A5, FUNCOP_1: 7

          .= 0 by NORMSP_0:def 6;

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

        end;

        then 0 <= r0 by A2;

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

        then (( BoundedLinearOperatorsNorm (X,Y)) . f) = 0 by Th29;

        hence thesis;

      end;

    end;

    registration

      let X,Y be ComplexNormSpace;

      cluster -> Function-like Relation-like for Element of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      coherence ;

    end

    definition

      let X,Y be ComplexNormSpace;

      let f be Element of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      let v be VECTOR of X;

      :: original: .

      redefine

      func f . v -> VECTOR of Y ;

      coherence

      proof

        reconsider f as LinearOperator of X, Y by Def7;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: CLOPBAN1:34

    

     Th34: for X,Y be ComplexNormSpace, f,g,h be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) holds h = (f + g) iff for x be VECTOR of X holds (h . x) = ((f . x) + (g . x))

    proof

      let X,Y be ComplexNormSpace;

      let f,g,h be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      reconsider f1 = f, g1 = g, h1 = h as VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

      h = (f + g) iff h1 = (f1 + g1);

      hence thesis by Th23;

    end;

    theorem :: CLOPBAN1:35

    

     Th35: for X,Y be ComplexNormSpace, f,h be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)), c be Complex holds h = (c * f) iff for x be VECTOR of X holds (h . x) = (c * (f . x))

    proof

      let X,Y be ComplexNormSpace;

      let f,h be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      let c be Complex;

      reconsider f1 = f as VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

      reconsider h1 = h as VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

       A1:

      now

        assume h1 = (c * f1);

        

        hence h = (( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))) . [c, f1]) by CLVECT_1:def 1

        .= (c * f) by CLVECT_1:def 1;

      end;

      now

        assume h = (c * f);

        

        hence h1 = (( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))) . [c, f]) by CLVECT_1:def 1

        .= (c * f1) by CLVECT_1:def 1;

      end;

      hence thesis by A1, Th24;

    end;

    theorem :: CLOPBAN1:36

    

     Th36: for X,Y be ComplexNormSpace, f,g be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)), c be Complex holds ( ||.f.|| = 0 iff f = ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)))) & ||.(c * f).|| = ( |.c.| * ||.f.||) & ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

    proof

      let X,Y be ComplexNormSpace;

      let f,g be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      let c be Complex;

       A1:

      now

        assume

         A2: f = ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)));

        thus ||.f.|| = 0

        proof

          reconsider g = f as Lipschitzian LinearOperator of X, Y by Def7;

          set z = (the carrier of X --> ( 0. Y));

          reconsider z as Function of the carrier of X, the carrier of Y;

          consider r0 be object such that

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

          reconsider r0 as Real by A3;

          

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

          

           A5: ( PreNorms g) is non empty bounded_above by Th26;

          

           A6: z = g by A2, Th30;

           A7:

          now

            let r be Real;

            assume r in ( PreNorms g);

            then

            consider t be VECTOR of X such that

             A8: r = ||.(g . t).|| and ||.t.|| <= 1;

             ||.(g . t).|| = ||.( 0. Y).|| by A6, FUNCOP_1: 7

            .= 0 by NORMSP_0:def 6;

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

          end;

          then 0 <= r0 by A3;

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

          then (( BoundedLinearOperatorsNorm (X,Y)) . f) = 0 by Th29;

          hence thesis;

        end;

      end;

      

       A9: ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

      proof

        reconsider f1 = f, g1 = g, h1 = (f + g) as Lipschitzian LinearOperator of X, Y by Def7;

        

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

         A11:

        now

          let t be VECTOR of X such that

           A12: ||.t.|| <= 1;

           0 <= ||.g.|| by Th32;

          then

           A13: ( ||.g.|| * ||.t.||) <= ( ||.g.|| * 1) by A12, XREAL_1: 64;

           0 <= ||.f.|| by Th32;

          then ( ||.f.|| * ||.t.||) <= ( ||.f.|| * 1) by A12, XREAL_1: 64;

          then

           A14: (( ||.f.|| * ||.t.||) + ( ||.g.|| * ||.t.||)) <= (( ||.f.|| * 1) + ( ||.g.|| * 1)) by A13, XREAL_1: 7;

          

           A15: ||.((f1 . t) + (g1 . t)).|| <= ( ||.(f1 . t).|| + ||.(g1 . t).||) by CLVECT_1:def 13;

          

           A16: ||.(g1 . t).|| <= ( ||.g.|| * ||.t.||) by Th31;

           ||.(f1 . t).|| <= ( ||.f.|| * ||.t.||) by Th31;

          then ( ||.(f1 . t).|| + ||.(g1 . t).||) <= (( ||.f.|| * ||.t.||) + ( ||.g.|| * ||.t.||)) by A16, XREAL_1: 7;

          then

           A17: ( ||.(f1 . t).|| + ||.(g1 . t).||) <= ( ||.f.|| + ||.g.||) by A14, XXREAL_0: 2;

           ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| by Th34;

          hence ||.(h1 . t).|| <= ( ||.f.|| + ||.g.||) by A15, A17, XXREAL_0: 2;

        end;

         A18:

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then ex t be VECTOR of X st r = ||.(h1 . t).|| & ||.t.|| <= 1;

          hence r <= ( ||.f.|| + ||.g.||) by A11;

        end;

        (( BoundedLinearOperatorsNorm (X,Y)) . (f + g)) = ( upper_bound ( PreNorms h1)) by Th29;

        hence thesis by A18, A10;

      end;

      

       A19: ||.(c * f).|| = ( |.c.| * ||.f.||)

      proof

        reconsider f1 = f, h1 = (c * f) as Lipschitzian LinearOperator of X, Y by Def7;

        

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

         A21:

        now

          

           A22: 0 <= ||.f.|| by Th32;

          let t be VECTOR of X;

          assume ||.t.|| <= 1;

          then

           A23: ( ||.f.|| * ||.t.||) <= ( ||.f.|| * 1) by A22, XREAL_1: 64;

           ||.(f1 . t).|| <= ( ||.f.|| * ||.t.||) by Th31;

          then

           A24: ||.(f1 . t).|| <= ||.f.|| by A23, XXREAL_0: 2;

          

           A25: ||.(c * (f1 . t)).|| = ( |.c.| * ||.(f1 . t).||) by CLVECT_1:def 13;

          

           A26: 0 <= |.c.| by COMPLEX1: 46;

           ||.(h1 . t).|| = ||.(c * (f1 . t)).|| by Th35;

          hence ||.(h1 . t).|| <= ( |.c.| * ||.f.||) by A25, A24, A26, XREAL_1: 64;

        end;

         A27:

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then ex t be VECTOR of X st r = ||.(h1 . t).|| & ||.t.|| <= 1;

          hence r <= ( |.c.| * ||.f.||) by A21;

        end;

         A28:

        now

          per cases ;

            case

             A29: c <> 0c ;

             A30:

            now

              

               A31: 0 <= ||.(c * f).|| by Th32;

              let t be VECTOR of X;

              assume ||.t.|| <= 1;

              then

               A32: ( ||.(c * f).|| * ||.t.||) <= ( ||.(c * f).|| * 1) by A31, XREAL_1: 64;

               ||.(h1 . t).|| <= ( ||.(c * f).|| * ||.t.||) by Th31;

              then

               A33: ||.(h1 . t).|| <= ||.(c * f).|| by A32, XXREAL_0: 2;

              (h1 . t) = (c * (f1 . t)) by Th35;

              

              then

               A34: ((c " ) * (h1 . t)) = (((c " ) * c) * (f1 . t)) by CLVECT_1:def 4

              .= ( 1r * (f1 . t)) by A29, COMPLEX1:def 4, XCMPLX_0:def 7

              .= (f1 . t) by CLVECT_1:def 5;

              

               A35: |.(c " ).| = ( |.c.| " ) by COMPLEX1: 66;

              

               A36: 0 <= |.(c " ).| by COMPLEX1: 46;

               ||.((c " ) * (h1 . t)).|| = ( |.(c " ).| * ||.(h1 . t).||) by CLVECT_1:def 13;

              hence ||.(f1 . t).|| <= (( |.c.| " ) * ||.(c * f).||) by A34, A33, A36, A35, XREAL_1: 64;

            end;

             A37:

            now

              let r be Real;

              assume r in ( PreNorms f1);

              then ex t be VECTOR of X st r = ||.(f1 . t).|| & ||.t.|| <= 1;

              hence r <= (( |.c.| " ) * ||.(c * f).||) by A30;

            end;

            

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

            

             A39: 0 <= |.c.| by COMPLEX1: 46;

            (( BoundedLinearOperatorsNorm (X,Y)) . f) = ( upper_bound ( PreNorms f1)) by Th29;

            then ||.f.|| <= (( |.c.| " ) * ||.(c * f).||) by A37, A38;

            then ( |.c.| * ||.f.||) <= ( |.c.| * (( |.c.| " ) * ||.(c * f).||)) by A39, XREAL_1: 64;

            then

             A40: ( |.c.| * ||.f.||) <= (( |.c.| * ( |.c.| " )) * ||.(c * f).||);

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

            then ( |.c.| * ||.f.||) <= (1 * ||.(c * f).||) by A40, XCMPLX_0:def 7;

            hence ( |.c.| * ||.f.||) <= ||.(c * f).||;

          end;

            case

             A41: c = 0c ;

            reconsider fz = f as VECTOR of ( C_VectorSpace_of_BoundedLinearOperators (X,Y));

            (c * f) = (( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))) . [c, f]) by CLVECT_1:def 1

            .= (c * fz) by CLVECT_1:def 1

            .= ( 0. ( C_VectorSpace_of_BoundedLinearOperators (X,Y))) by A41, CLVECT_1: 1

            .= ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)));

            hence thesis by A41, Th33, COMPLEX1: 44;

          end;

        end;

        (( BoundedLinearOperatorsNorm (X,Y)) . (c * f)) = ( upper_bound ( PreNorms h1)) by Th29;

        then ||.(c * f).|| <= ( |.c.| * ||.f.||) by A27, A20;

        hence thesis by A28, XXREAL_0: 1;

      end;

      now

        reconsider g = f as Lipschitzian LinearOperator of X, Y by Def7;

        set z = (the carrier of X --> ( 0. Y));

        reconsider z as Function of the carrier of X, the carrier of Y;

        assume

         A42: ||.f.|| = 0 ;

        now

          let t be VECTOR of X;

           ||.(g . t).|| <= ( ||.f.|| * ||.t.||) by Th31;

          then ||.(g . t).|| = 0 by A42, CLVECT_1: 105;

          

          hence (g . t) = ( 0. Y) by NORMSP_0:def 5

          .= (z . t) by FUNCOP_1: 7;

        end;

        then g = z by FUNCT_2: 63;

        hence f = ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y))) by Th30;

      end;

      hence thesis by A1, A19, A9;

    end;

    theorem :: CLOPBAN1:37

    

     Th37: for X,Y be ComplexNormSpace holds ( C_NormSpace_of_BoundedLinearOperators (X,Y)) is reflexive discerning ComplexNormSpace-like

    proof

      let X,Y be ComplexNormSpace;

      thus ( C_NormSpace_of_BoundedLinearOperators (X,Y)) is reflexive by Th36;

      for x,y be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) holds for c be Complex holds ( ||.x.|| = 0 iff x = ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)))) & ||.(c * x).|| = ( |.c.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Th36;

      hence thesis by CLVECT_1:def 13;

    end;

    theorem :: CLOPBAN1:38

    

     Th38: for X,Y be ComplexNormSpace holds ( C_NormSpace_of_BoundedLinearOperators (X,Y)) is ComplexNormSpace

    proof

      let X,Y be ComplexNormSpace;

       CLSStruct (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( C_VectorSpace_of_LinearOperators (X,Y)))) #) is ComplexLinearSpace;

      hence thesis by Th37, CSSPACE3: 2;

    end;

    registration

      let X,Y be ComplexNormSpace;

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

      coherence by Th38;

    end

    theorem :: CLOPBAN1:39

    

     Th39: for X,Y be ComplexNormSpace, f,g,h be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) holds h = (f - g) iff for x be VECTOR of X holds (h . x) = ((f . x) - (g . x))

    proof

      let X,Y be ComplexNormSpace;

      let f,g,h be Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y));

      reconsider f9 = f, g9 = g, h9 = h as Lipschitzian LinearOperator of X, Y by Def7;

      hereby

        assume h = (f - g);

        then (h + g) = (f - (g - g)) by RLVECT_1: 29;

        then (h + g) = (f - ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)))) by RLVECT_1: 15;

        then

         A1: (h + g) = f by RLVECT_1: 13;

        now

          let x be VECTOR of X;

          (f9 . x) = ((h9 . x) + (g9 . x)) by A1, Th34;

          then ((f9 . x) - (g9 . x)) = ((h9 . x) + ((g9 . x) - (g9 . x))) by RLVECT_1:def 3;

          then ((f9 . x) - (g9 . x)) = ((h9 . x) + ( 0. Y)) by RLVECT_1: 15;

          hence ((f9 . x) - (g9 . x)) = (h9 . x) by RLVECT_1: 4;

        end;

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

      end;

      assume

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

      now

        let x be VECTOR of X;

        (h9 . x) = ((f9 . x) - (g9 . x)) by A2;

        then ((h9 . x) + (g9 . x)) = ((f9 . x) - ((g9 . x) - (g9 . x))) by RLVECT_1: 29;

        then ((h9 . x) + (g9 . x)) = ((f9 . x) - ( 0. Y)) by RLVECT_1: 15;

        hence ((h9 . x) + (g9 . x)) = (f9 . x) by RLVECT_1: 13;

      end;

      then f = (h + g) by Th34;

      then (f - g) = (h + (g - g)) by RLVECT_1:def 3;

      then (f - g) = (h + ( 0. ( C_NormSpace_of_BoundedLinearOperators (X,Y)))) by RLVECT_1: 15;

      hence thesis by RLVECT_1: 4;

    end;

    begin

    definition

      let X be ComplexNormSpace;

      :: CLOPBAN1:def13

      attr X is complete means

      : Def13: for seq be sequence of X holds seq is Cauchy_sequence_by_Norm implies seq is convergent;

    end

    registration

      cluster complete for ComplexNormSpace;

      existence by Def13, CSSPACE3: 9;

    end

    definition

      mode ComplexBanachSpace is complete ComplexNormSpace;

    end

    

     Lm2: for e be Real, seq be Real_Sequence st (seq is convergent & ex k be Nat st for i be Nat st k <= i holds (seq . i) <= e) holds ( lim seq) <= e

    proof

      let e be Real;

      let seq be Real_Sequence such that

       A1: seq is convergent and

       A2: ex k be Nat st for i be Nat st k <= i holds (seq . i) <= e;

      consider k be Nat such that

       A3: for i be Nat st k <= i holds (seq . i) <= e by A2;

      reconsider e as Element of REAL by XREAL_0:def 1;

      set cseq = ( seq_const e);

      

       A4: ( lim cseq) = (cseq . 0 ) by SEQ_4: 26

      .= e by SEQ_1: 57;

       A5:

      now

        let i be Nat;

        

         A6: ((seq ^\ k) . i) = (seq . (k + i)) by NAT_1:def 3;

        (seq . (k + i)) <= e by A3, NAT_1: 11;

        hence ((seq ^\ k) . i) <= (cseq . i) by A6, SEQ_1: 57;

      end;

      ( lim (seq ^\ k)) = ( lim seq) by A1, SEQ_4: 20;

      hence thesis by A1, A5, A4, SEQ_2: 18;

    end;

    theorem :: CLOPBAN1:40

    

     Th40: for X be ComplexNormSpace, seq be sequence of X st seq is convergent holds ||.seq.|| is convergent & ( lim ||.seq.||) = ||.( lim seq).||

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X such that

       A1: seq is convergent;

       A2:

      now

        let e1 be Real such that

         A3: e1 > 0 ;

        reconsider e = e1 as Real;

        consider k be Nat such that

         A4: for n be Nat st n >= k holds ||.((seq . n) - ( lim seq)).|| < e by A1, A3, CLVECT_1:def 16;

        take k;

        now

          let m be Nat;

          assume m >= k;

          then

           A5: ||.((seq . m) - ( lim seq)).|| < e by A4;

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

          then |.(( ||.seq.|| . m) - ||.( lim seq).||).| <= ||.((seq . m) - ( lim seq)).|| by CLVECT_1: 110;

          hence |.(( ||.seq.|| . m) - ||.( lim seq).||).| < e1 by A5, XXREAL_0: 2;

        end;

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

      end;

      then ||.seq.|| is convergent by SEQ_2:def 6;

      hence thesis by A2, SEQ_2:def 7;

    end;

    theorem :: CLOPBAN1:41

    

     Th41: for X,Y be ComplexNormSpace st Y is complete holds for seq be sequence of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent

    proof

      let X,Y be ComplexNormSpace such that

       A1: Y is complete;

      let vseq be sequence of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) such that

       A2: vseq is Cauchy_sequence_by_Norm;

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

      

       A3: for x be Element of X holds ex y be Element of Y st P[x, y]

      proof

        let x be Element of X;

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

        consider xseq be sequence of Y such that

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

        

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

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A4;

        end;

        take ( lim xseq);

        

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

        proof

          let m,k be Nat;

          

           A7: k in NAT by ORDINAL1:def 12;

          

           A8: m in NAT by ORDINAL1:def 12;

          reconsider h1 = ((vseq . m) - (vseq . k)) as Lipschitzian LinearOperator of X, Y by Def7;

          

           A9: (xseq . k) = (( modetrans ((vseq . k),X,Y)) . x) by A4, A7;

          (vseq . m) is Lipschitzian LinearOperator of X, Y by Def7;

          then

           A10: ( modetrans ((vseq . m),X,Y)) = (vseq . m) by Th28;

          (vseq . k) is Lipschitzian LinearOperator of X, Y by Def7;

          then

           A11: ( modetrans ((vseq . k),X,Y)) = (vseq . k) by Th28;

          (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A4, A8;

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

          hence thesis by Th31;

        end;

        now

          let e be Real such that

           A12: e > 0 ;

          now

            per cases ;

              case

               A13: x = ( 0. X);

              take k = 0 ;

              thus for n,m be Nat st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e

              proof

                let n,m be Nat such that n >= k and m >= k;

                

                 A14: n in NAT by ORDINAL1:def 12;

                

                 A15: m in NAT by ORDINAL1:def 12;

                

                 A16: (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A4, A15

                .= (( modetrans ((vseq . m),X,Y)) . ( 0c * x)) by A13, CLVECT_1: 1

                .= ( 0c * (( modetrans ((vseq . m),X,Y)) . x)) by Def3

                .= ( 0. Y) by CLVECT_1: 1;

                (xseq . n) = (( modetrans ((vseq . n),X,Y)) . x) by A4, A14

                .= (( modetrans ((vseq . n),X,Y)) . ( 0c * x)) by A13, CLVECT_1: 1

                .= ( 0c * (( modetrans ((vseq . n),X,Y)) . x)) by Def3

                .= ( 0. Y) by CLVECT_1: 1;

                

                then ||.((xseq . n) - (xseq . m)).|| = ||.( 0. Y).|| by A16, RLVECT_1: 13

                .= 0 by NORMSP_0:def 6;

                hence thesis by A12;

              end;

            end;

              case x <> ( 0. X);

              then

               A17: ||.x.|| <> 0 by NORMSP_0:def 5;

              then

               A18: ||.x.|| > 0 by CLVECT_1: 105;

              then

              consider k be Nat such that

               A19: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < (e / ||.x.||) by A2, A12, CSSPACE3: 8;

              take k;

              thus for n,m be Nat st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e

              proof

                let n,m be Nat such that

                 A20: n >= k and

                 A21: m >= k;

                 ||.((vseq . n) - (vseq . m)).|| < (e / ||.x.||) by A19, A20, A21;

                then

                 A22: ( ||.((vseq . n) - (vseq . m)).|| * ||.x.||) < ((e / ||.x.||) * ||.x.||) by A18, XREAL_1: 68;

                

                 A23: ((e / ||.x.||) * ||.x.||) = ((e * ( ||.x.|| " )) * ||.x.||) by XCMPLX_0:def 9

                .= (e * (( ||.x.|| " ) * ||.x.||))

                .= (e * 1) by A17, XCMPLX_0:def 7

                .= e;

                 ||.((xseq . n) - (xseq . m)).|| <= ( ||.((vseq . n) - (vseq . m)).|| * ||.x.||) by A6;

                hence thesis by A22, A23, XXREAL_0: 2;

              end;

            end;

          end;

          hence ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e;

        end;

        then xseq is Cauchy_sequence_by_Norm by CSSPACE3: 8;

        then xseq is convergent by A1;

        hence thesis by A5;

      end;

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

       A24: for x be Element of X holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

      reconsider tseq = f as Function of X, Y;

       A25:

      now

        let x,y be VECTOR of X;

        consider xseq be sequence of Y such that

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

         A27: xseq is convergent and

         A28: (tseq . x) = ( lim xseq) by A24;

        consider zseq be sequence of Y such that

         A29: for n be Nat holds (zseq . n) = (( modetrans ((vseq . n),X,Y)) . (x + y)) and zseq is convergent and

         A30: (tseq . (x + y)) = ( lim zseq) by A24;

        consider yseq be sequence of Y such that

         A31: for n be Nat holds (yseq . n) = (( modetrans ((vseq . n),X,Y)) . y) and

         A32: yseq is convergent and

         A33: (tseq . y) = ( lim yseq) by A24;

        now

          let n be Nat;

          

          thus (zseq . n) = (( modetrans ((vseq . n),X,Y)) . (x + y)) by A29

          .= ((( modetrans ((vseq . n),X,Y)) . x) + (( modetrans ((vseq . n),X,Y)) . y)) by VECTSP_1:def 20

          .= ((xseq . n) + (( modetrans ((vseq . n),X,Y)) . y)) by A26

          .= ((xseq . n) + (yseq . n)) by A31;

        end;

        then zseq = (xseq + yseq) by NORMSP_1:def 2;

        hence (tseq . (x + y)) = ((tseq . x) + (tseq . y)) by A27, A28, A32, A33, A30, CLVECT_1: 119;

      end;

      now

        let x be VECTOR of X;

        let c be Complex;

        consider xseq be sequence of Y such that

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

         A35: xseq is convergent and

         A36: (tseq . x) = ( lim xseq) by A24;

        consider zseq be sequence of Y such that

         A37: for n be Nat holds (zseq . n) = (( modetrans ((vseq . n),X,Y)) . (c * x)) and zseq is convergent and

         A38: (tseq . (c * x)) = ( lim zseq) by A24;

        now

          let n be Nat;

          

          thus (zseq . n) = (( modetrans ((vseq . n),X,Y)) . (c * x)) by A37

          .= (c * (( modetrans ((vseq . n),X,Y)) . x)) by Def3

          .= (c * (xseq . n)) by A34;

        end;

        then zseq = (c * xseq) by CLVECT_1:def 14;

        hence (tseq . (c * x)) = (c * (tseq . x)) by A35, A36, A38, CLVECT_1: 122;

      end;

      then

      reconsider tseq as LinearOperator of X, Y by A25, Def3, VECTSP_1:def 20;

      now

        let e1 be Real such that

         A39: e1 > 0 ;

        reconsider e = e1 as Real;

        consider k be Nat such that

         A40: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, A39, CSSPACE3: 8;

        take k;

        now

          let m be Nat;

          assume m >= k;

          then

           A41: ||.((vseq . m) - (vseq . k)).|| < e by A40;

          

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

          

           A43: ||.(vseq . k).|| = ( ||.vseq.|| . k) by NORMSP_0:def 4;

           |.( ||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| by CLVECT_1: 110;

          hence |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1 by A43, A42, A41, XXREAL_0: 2;

        end;

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

      end;

      then

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

      

       A45: tseq is Lipschitzian

      proof

        take ( lim ||.vseq.||);

         A46:

        now

          let x be VECTOR of X;

          consider xseq be sequence of Y such that

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

           A48: xseq is convergent and

           A49: (tseq . x) = ( lim xseq) by A24;

          

           A50: ||.(tseq . x).|| = ( lim ||.xseq.||) by A48, A49, Th19;

          

           A51: for m be Nat holds ||.(xseq . m).|| <= ( ||.(vseq . m).|| * ||.x.||)

          proof

            let m be Nat;

            

             A52: (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A47;

            (vseq . m) is Lipschitzian LinearOperator of X, Y by Def7;

            hence thesis by A52, Th28, Th31;

          end;

          

           A53: for n be Nat holds ( ||.xseq.|| . n) <= (( ||.x.|| (#) ||.vseq.||) . n)

          proof

            let n be Nat;

            

             A54: ( ||.xseq.|| . n) = ||.(xseq . n).|| by NORMSP_0:def 4;

            

             A55: ||.(vseq . n).|| = ( ||.vseq.|| . n) by NORMSP_0:def 4;

             ||.(xseq . n).|| <= ( ||.(vseq . n).|| * ||.x.||) by A51;

            hence thesis by A54, A55, SEQ_1: 9;

          end;

          

           A56: ( ||.x.|| (#) ||.vseq.||) is convergent by A44;

          

           A57: ( lim ( ||.x.|| (#) ||.vseq.||)) = (( lim ||.vseq.||) * ||.x.||) by A44, SEQ_2: 8;

           ||.xseq.|| is convergent by A48, A49, Th19;

          hence ||.(tseq . x).|| <= (( lim ||.vseq.||) * ||.x.||) by A50, A53, A56, A57, SEQ_2: 18;

        end;

        now

          let n be Nat;

           ||.(vseq . n).|| >= 0 by CLVECT_1: 105;

          hence ( ||.vseq.|| . n) >= 0 by NORMSP_0:def 4;

        end;

        hence thesis by A44, A46, SEQ_2: 17;

      end;

      

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

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

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

        take k;

        now

          let n be Nat such that

           A60: n >= k;

          now

            let x be VECTOR of X;

            consider xseq be sequence of Y such that

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

             A62: xseq is convergent and

             A63: (tseq . x) = ( lim xseq) by A24;

            

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

            proof

              let m,k be Nat;

              reconsider h1 = ((vseq . m) - (vseq . k)) as Lipschitzian LinearOperator of X, Y by Def7;

              

               A65: (xseq . k) = (( modetrans ((vseq . k),X,Y)) . x) by A61;

              (vseq . m) is Lipschitzian LinearOperator of X, Y by Def7;

              then

               A66: ( modetrans ((vseq . m),X,Y)) = (vseq . m) by Th28;

              (vseq . k) is Lipschitzian LinearOperator of X, Y by Def7;

              then

               A67: ( modetrans ((vseq . k),X,Y)) = (vseq . k) by Th28;

              (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A61;

              then ((xseq . m) - (xseq . k)) = (h1 . x) by A66, A67, A65, Th39;

              hence thesis by Th31;

            end;

            

             A68: for m be Nat st m >= k holds ||.((xseq . n) - (xseq . m)).|| <= (e * ||.x.||)

            proof

              let m be Nat;

              assume m >= k;

              then

               A69: ||.((vseq . n) - (vseq . m)).|| < e by A59, A60;

              

               A70: ||.((xseq . n) - (xseq . m)).|| <= ( ||.((vseq . n) - (vseq . m)).|| * ||.x.||) by A64;

               0 <= ||.x.|| by CLVECT_1: 105;

              then ( ||.((vseq . n) - (vseq . m)).|| * ||.x.||) <= (e * ||.x.||) by A69, XREAL_1: 64;

              hence thesis by A70, XXREAL_0: 2;

            end;

             ||.((xseq . n) - (tseq . x)).|| <= (e * ||.x.||)

            proof

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

              consider rseq be Real_Sequence such that

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

              now

                let x be object;

                assume x in NAT ;

                then

                reconsider k = x as Nat;

                

                thus (rseq . x) = ||.((xseq . k) - (xseq . n)).|| by A71

                .= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 4

                .= ( ||.(xseq - (xseq . n)).|| . x) by NORMSP_0:def 4;

              end;

              then

               A72: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2: 12;

              

               A73: (xseq - (xseq . n)) is convergent by A62, CLVECT_1: 115;

              ( lim (xseq - (xseq . n))) = ((tseq . x) - (xseq . n)) by A62, A63, CLVECT_1: 121;

              then

               A74: ( lim rseq) = ||.((tseq . x) - (xseq . n)).|| by A73, A72, Th40;

              for m be Nat st m >= k holds (rseq . m) <= (e * ||.x.||)

              proof

                let m be Nat such that

                 A75: m >= k;

                (rseq . m) = ||.((xseq . m) - (xseq . n)).|| by A71

                .= ||.((xseq . n) - (xseq . m)).|| by CLVECT_1: 108;

                hence thesis by A68, A75;

              end;

              then ( lim rseq) <= (e * ||.x.||) by A73, A72, Lm2, Th40;

              hence thesis by A74, CLVECT_1: 108;

            end;

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

          end;

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

        end;

        hence thesis;

      end;

      reconsider tseq as Lipschitzian LinearOperator of X, Y by A45;

      reconsider tv = tseq as Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) by Def7;

      

       A76: 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 such that

         A77: e > 0 ;

        consider k be Nat such that

         A78: for n be Nat st n >= k holds for x be VECTOR of X holds ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= (e * ||.x.||) by A58, A77;

        now

          set g1 = tseq;

          let n be Nat such that

           A79: n >= k;

          reconsider h1 = ((vseq . n) - tv) as Lipschitzian LinearOperator of X, Y by Def7;

          set f1 = ( modetrans ((vseq . n),X,Y));

           A80:

          now

            let t be VECTOR of X;

            assume ||.t.|| <= 1;

            then

             A81: (e * ||.t.||) <= (e * 1) by A77, XREAL_1: 64;

            

             A82: ||.((f1 . t) - (g1 . t)).|| <= (e * ||.t.||) by A78, A79;

            (vseq . n) is Lipschitzian LinearOperator of X, Y by Def7;

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

            then ||.(h1 . t).|| = ||.((f1 . t) - (g1 . t)).|| by Th39;

            hence ||.(h1 . t).|| <= e by A82, A81, XXREAL_0: 2;

          end;

           A83:

          now

            let r be Real;

            assume r in ( PreNorms h1);

            then ex t be VECTOR of X st r = ||.(h1 . t).|| & ||.t.|| <= 1;

            hence r <= e by A80;

          end;

          

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

          (( BoundedLinearOperatorsNorm (X,Y)) . ((vseq . n) - tv)) = ( upper_bound ( PreNorms h1)) by Th29;

          hence ||.((vseq . n) - tv).|| <= e by A83, A84;

        end;

        hence thesis;

      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

         A85: e > 0 ;

        reconsider ee = e as Real;

        consider m be Nat such that

         A86: for n be Nat st n >= m holds ||.((vseq . n) - tv).|| <= (ee / 2) by A76, A85;

        

         A87: (e / 2) < e by A85, XREAL_1: 216;

        now

          let n be Nat;

          assume n >= m;

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

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

        end;

        hence thesis;

      end;

      hence thesis by CLVECT_1:def 15;

    end;

    theorem :: CLOPBAN1:42

    

     Th42: for X be ComplexNormSpace, Y be ComplexBanachSpace holds ( C_NormSpace_of_BoundedLinearOperators (X,Y)) is ComplexBanachSpace

    proof

      let X be ComplexNormSpace;

      let Y be ComplexBanachSpace;

      for seq be sequence of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th41;

      hence thesis by Def13;

    end;

    registration

      let X be ComplexNormSpace;

      let Y be ComplexBanachSpace;

      cluster ( C_NormSpace_of_BoundedLinearOperators (X,Y)) -> complete;

      coherence by Th42;

    end