lopban_1.miz



    begin

    definition

      let X be set;

      let Y be non empty set;

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

      let a be Real, f be Function of X, Y;

      :: original: [;]

      redefine

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

      coherence

      proof

        

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

        a in REAL by XREAL_0:def 1;

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

        then

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

        (F [;] (a,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 non empty addLoopStr;

      :: LOPBAN_1:def1

      func FuncAdd (X,Y) -> BinOp of ( Funcs (X,the carrier of Y)) means

      : Def1: for f,g be Element of ( Funcs (X,the carrier of Y)) holds (it . (f,g)) = (the addF of Y .: (f,g));

      existence

      proof

        deffunc F( Element of ( Funcs (X,the carrier of Y)), Element of ( Funcs (X,the carrier of Y))) = (the addF of Y .: ($1,$2));

        thus ex ADD be BinOp of ( Funcs (X,the carrier of Y)) st for f,g be Element of ( Funcs (X,the carrier of Y)) holds (ADD . (f,g)) = F(f,g) from BINOP_1:sch 4;

      end;

      uniqueness

      proof

        let it1,it2 be BinOp of ( Funcs (X,the carrier of Y)) such that

         A1: for f,g be Element of ( Funcs (X,the carrier of Y)) holds (it1 . (f,g)) = (the addF of Y .: (f,g)) and

         A2: for f,g be Element of ( Funcs (X,the carrier of Y)) holds (it2 . (f,g)) = (the addF of Y .: (f,g));

        now

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

          

          thus (it1 . (f,g)) = (the addF of Y .: (f,g)) by A1

          .= (it2 . (f,g)) by A2;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty set;

      let Y be RealLinearSpace;

      :: LOPBAN_1:def2

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

      : Def2: for a be Real, f be Element of ( Funcs (X,the carrier of Y)), x be Element of X holds ((it . [a, f]) . x) = (a * (f . x));

      existence

      proof

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

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

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

        take F;

        let a be Real, f be Element of ( Funcs (X,the carrier of Y)), x be Element of X;

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

        

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

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

        hence thesis by A2, FUNCOP_1: 32;

      end;

      uniqueness

      proof

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

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

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

        now

          let a be Element of REAL , f be Element of ( Funcs (X,the carrier of Y));

          now

            let x be Element of X;

            

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

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

          end;

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

        end;

        hence thesis;

      end;

    end

    definition

      let X be set;

      let Y be non empty ZeroStr;

      :: LOPBAN_1:def3

      func FuncZero (X,Y) -> Element of ( Funcs (X,the carrier of Y)) equals (X --> ( 0. Y));

      coherence by FUNCT_2: 8;

    end

    reserve X for non empty set;

    reserve Y for RealLinearSpace;

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

    

     Lm1: for A,B be non empty set holds for x be Element of A, f be Function of A, B holds x in ( dom f)

    proof

      let A,B be non empty set;

      let x be Element of A, f be Function of A, B;

      x in A;

      hence thesis by FUNCT_2:def 1;

    end;

    theorem :: LOPBAN_1:1

    

     Th1: for Y be non empty addLoopStr, f,g,h be Element of ( Funcs (X,the carrier of Y)) holds h = (( FuncAdd (X,Y)) . (f,g)) iff for x be Element of X holds (h . x) = ((f . x) + (g . x))

    proof

      let Y be non empty addLoopStr, f,g,h be Element of ( Funcs (X,the carrier of Y));

      hereby

        assume

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

        let x be Element of X;

        

         A2: x in ( dom (the addF of Y .: (f,g))) by Lm1;

        

        thus (h . x) = ((the addF of Y .: (f,g)) . x) by A1, Def1

        .= ((f . x) + (g . x)) by A2, FUNCOP_1: 22;

      end;

      assume

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

      now

        let x be Element of X;

        

         A4: x in ( dom (the addF of Y .: (f,g))) by Lm1;

        

        thus ((( FuncAdd (X,Y)) . (f,g)) . x) = ((the addF of Y .: (f,g)) . x) by Def1

        .= ((f . x) + (g . x)) by A4, FUNCOP_1: 22

        .= (h . x) by A3;

      end;

      hence h = (( FuncAdd (X,Y)) . (f,g)) by FUNCT_2: 63;

    end;

    reserve a,b for Real;

    theorem :: LOPBAN_1: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 Def2;

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

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

        end;

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

      end;

      hence thesis;

    end;

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

    theorem :: LOPBAN_1: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 Th1

        .= ((( FuncAdd (X,Y)) . (g,f)) . x) by Th1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_1: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 Th1

        .= ((f . x) + ((g . x) + (h . x))) by Th1

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

        .= (((( FuncAdd (X,Y)) . (f,g)) . x) + (h . x)) by Th1

        .= ((( FuncAdd (X,Y)) . ((( FuncAdd (X,Y)) . (f,g)),h)) . x) by Th1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_1: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 Th1

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

        .= (f . x);

      end;

      hence thesis by FUNCT_2: 63;

    end;

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

    theorem :: LOPBAN_1:6

    

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

    proof

      now

        let x be Element of X;

        set y = (f . x);

        

        thus ((( FuncAdd (X,Y)) . (f,(( FuncExtMult (X,Y)) . [( - jj), f]))) . x) = ((f . x) + ((( FuncExtMult (X,Y)) . [( - jj), f]) . x)) by Th1

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

        .= ((f . x) + ( - y)) by RLVECT_1: 16

        .= ( 0. Y) by RLVECT_1: 5

        .= (( FuncZero (X,Y)) . x) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_1:7

    

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

    proof

      now

        let x be Element of X;

        

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_1:8

    

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

    proof

      reconsider a, b as Element of REAL by XREAL_0:def 1;

      now

        let x be Element of X;

        

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

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

        .= ((a * b) * (f . x)) by RLVECT_1:def 7

        .= ((( FuncExtMult (X,Y)) . [(a * b), f]) . x) by Th2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_1:9

    

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

    proof

      reconsider a, b as Element of REAL by XREAL_0:def 1;

      now

        let x be Element of X;

        

        thus ((( FuncAdd (X,Y)) . ((( FuncExtMult (X,Y)) . [a, f]),(( FuncExtMult (X,Y)) . [b, f]))) . x) = (((( FuncExtMult (X,Y)) . [a, f]) . x) + ((( FuncExtMult (X,Y)) . [b, f]) . x)) by Th1

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

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

        .= ((a + b) * (f . x)) by RLVECT_1:def 6

        .= ((( FuncExtMult (X,Y)) . [(a + b), f]) . x) by Th2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

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

    proof

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

      now

        let x be Element of X;

        

        thus ((( FuncAdd (X,Y)) . ((( FuncExtMult (X,Y)) . [a, f]),(( FuncExtMult (X,Y)) . [a, g]))) . x) = (((( FuncExtMult (X,Y)) . [a, f]) . x) + ((( FuncExtMult (X,Y)) . [a, g]) . x)) by Th1

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

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

        .= (a * ((f . x) + (g . x))) by RLVECT_1:def 5

        .= (a * ((( FuncAdd (X,Y)) . (f,g)) . x)) by Th1

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_1:10

    

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

    proof

      

       A1: for a,b be Real, v holds ((a * b) * v) = (a * (b * v)) by Th8;

      

       A2: for a,b be Real, v holds ((a + b) * v) = ((a * v) + (b * v)) by Th9;

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

      

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

      

       A4: IT is right_complementable

      proof

        let u;

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

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

        take w;

        thus thesis by Th6;

      end;

      

       A5: for a be Real, u, v holds (a * (u + v)) = ((a * u) + (a * v)) by Lm2;

      

       A6: (1 * v) = v by Th7;

      

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

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

      hence thesis by A3, A7, A4, A5, A2, A1, A6, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

    end;

    definition

      let X be non empty set;

      let Y be RealLinearSpace;

      :: LOPBAN_1:def4

      func RealVectSpace (X,Y) -> RealLinearSpace equals RLSStruct (# ( 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 RealLinearSpace;

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

      coherence ;

    end

    registration

      let X be non empty set;

      let Y be RealLinearSpace;

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

      coherence by MONOID_0: 80;

    end

    definition

      let X be non empty set;

      let Y be RealLinearSpace;

      let f be VECTOR of ( RealVectSpace (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 :: LOPBAN_1:11

    for X be non empty set holds for Y be RealLinearSpace holds for f,g,h be VECTOR of ( RealVectSpace (X,Y)) holds h = (f + g) iff for x be Element of X holds (h . x) = ((f . x) + (g . x)) by Th1;

    theorem :: LOPBAN_1:12

    for X be non empty set holds for Y be RealLinearSpace holds for f,h be VECTOR of ( RealVectSpace (X,Y)) holds for a be Real holds h = (a * f) iff for x be Element of X holds (h . x) = (a * (f . x)) by Th2;

    theorem :: LOPBAN_1:13

    for X be non empty set holds for Y be RealLinearSpace holds ( 0. ( RealVectSpace (X,Y))) = (X --> ( 0. Y));

    begin

    definition

      let X,Y be non empty RLSStruct;

      let IT be Function of X, Y;

      :: LOPBAN_1:def5

      attr IT is homogeneous means

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

    end

    registration

      let X be non empty RLSStruct;

      let Y be RealLinearSpace;

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

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

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

        end;

        hereby

          let x be VECTOR of X, r be Real;

          

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

          .= (r * ( 0. Y))

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

        end;

      end;

    end

    definition

      let X,Y be RealLinearSpace;

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

    end

    definition

      let X,Y be RealLinearSpace;

      :: LOPBAN_1:def6

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

      : Def6: 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 ( RealVectSpace (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 ( RealVectSpace (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 RealLinearSpace;

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

      coherence

      proof

        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, r be Real;

          

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

          .= (r * ( 0. Y))

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

          .= ((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, Def6;

        let x be object;

        assume x in ( LinearOperators (X,Y));

        hence thesis;

      end;

    end

    theorem :: LOPBAN_1:14

    

     Th14: for X,Y be RealLinearSpace holds ( LinearOperators (X,Y)) is linearly-closed

    proof

      let X,Y be RealLinearSpace;

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

      

       A1: for v,u be VECTOR of ( RealVectSpace (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 ( RealVectSpace (the carrier of X,Y)) such that

         A2: v in W and

         A3: u in W;

        (v + u) is LinearOperator of X, Y

        proof

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

          

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

            

             A5: u9 is LinearOperator of X, Y by A3, Def6;

            

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

            

            thus (f . (s * x)) = ((u9 . (s * x)) + (v9 . (s * x))) by Th1

            .= ((s * (u9 . x)) + (v9 . (s * x))) by A5, Def5

            .= ((s * (u9 . x)) + (s * (v9 . x))) by A6, Def5

            .= (s * ((u9 . x) + (v9 . x))) by RLVECT_1:def 5

            .= (s * (f . x)) by Th1;

          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;

            

             A7: u9 is LinearOperator of X, Y by A3, Def6;

            

             A8: v9 is LinearOperator of X, Y by A2, Def6;

            

            thus (f . (x + y)) = ((u9 . (x + y)) + (v9 . (x + y))) by Th1

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

            .= (((u9 . x) + (u9 . y)) + ((v9 . x) + (v9 . y))) by A8, 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 Th1

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

            .= ((f . x) + (f . y)) by Th1;

          end;

          hence thesis by A4;

        end;

        hence thesis by Def6;

      end;

      for a be Real holds for v be VECTOR of ( RealVectSpace (the carrier of X,Y)) st v in W holds (a * v) in W

      proof

        let a be Real;

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

         A9: v in W;

        (a * v) is LinearOperator of X, Y

        proof

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

          

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

            

             A11: v9 is LinearOperator of X, Y by A9, Def6;

            

            thus (f . (s * x)) = (a * (v9 . (s * x))) by Th2

            .= (a * (s * (v9 . x))) by A11, Def5

            .= ((a * s) * (v9 . x)) by RLVECT_1:def 7

            .= (s * (a * (v9 . x))) by RLVECT_1:def 7

            .= (s * (f . x)) by 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;

            

             A12: v9 is LinearOperator of X, Y by A9, Def6;

            

            thus (f . (x + y)) = (a * (v9 . (x + y))) by Th2

            .= (a * ((v9 . x) + (v9 . y))) by A12, VECTSP_1:def 20

            .= ((a * (v9 . x)) + (a * (v9 . y))) by RLVECT_1:def 5

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

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

          end;

          hence thesis by A10;

        end;

        hence thesis by Def6;

      end;

      hence thesis by A1, RLSUB_1:def 1;

    end;

    theorem :: LOPBAN_1:15

    for X,Y be RealLinearSpace holds RLSStruct (# ( LinearOperators (X,Y)), ( Zero_ (( LinearOperators (X,Y)),( RealVectSpace (the carrier of X,Y)))), ( Add_ (( LinearOperators (X,Y)),( RealVectSpace (the carrier of X,Y)))), ( Mult_ (( LinearOperators (X,Y)),( RealVectSpace (the carrier of X,Y)))) #) is Subspace of ( RealVectSpace (the carrier of X,Y)) by Th14, RSSPACE: 11;

    registration

      let X,Y be RealLinearSpace;

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

      coherence by Th14, RSSPACE: 11;

    end

    definition

      let X,Y be RealLinearSpace;

      :: LOPBAN_1:def7

      func R_VectorSpace_of_LinearOperators (X,Y) -> RealLinearSpace equals RLSStruct (# ( LinearOperators (X,Y)), ( Zero_ (( LinearOperators (X,Y)),( RealVectSpace (the carrier of X,Y)))), ( Add_ (( LinearOperators (X,Y)),( RealVectSpace (the carrier of X,Y)))), ( Mult_ (( LinearOperators (X,Y)),( RealVectSpace (the carrier of X,Y)))) #);

      coherence ;

    end

    registration

      let X,Y be RealLinearSpace;

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

      coherence ;

    end

    registration

      let X,Y be RealLinearSpace;

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

      coherence by MONOID_0: 80;

    end

    definition

      let X,Y be RealLinearSpace;

      let f be Element of ( R_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 Def6;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: LOPBAN_1:16

    

     Th16: for X,Y be RealLinearSpace holds for f,g,h be VECTOR of ( R_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 RealLinearSpace;

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

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

      

       A1: ( R_VectorSpace_of_LinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of X,Y)) by Th14, RSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( RealVectSpace (the carrier of X,Y)) by RLSUB_1: 10;

      reconsider h1 = h as VECTOR of ( RealVectSpace (the carrier of X,Y)) by A1, RLSUB_1: 10;

      reconsider g1 = g as VECTOR of ( RealVectSpace (the carrier of X,Y)) by A1, RLSUB_1: 10;

       A2:

      now

        assume

         A3: h = (f + g);

        let x be Element of X;

        h1 = (f1 + g1) by A1, A3, RLSUB_1: 13;

        hence (h9 . x) = ((f9 . x) + (g9 . x)) by Th1;

      end;

      now

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

        then h1 = (f1 + g1) by Th1;

        hence h = (f + g) by A1, RLSUB_1: 13;

      end;

      hence thesis by A2;

    end;

    theorem :: LOPBAN_1:17

    

     Th17: for X,Y be RealLinearSpace holds for f,h be VECTOR of ( R_VectorSpace_of_LinearOperators (X,Y)) holds for a be Real holds h = (a * f) iff for x be VECTOR of X holds (h . x) = (a * (f . x))

    proof

      let X,Y be RealLinearSpace;

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

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

      let a be Real;

      

       A1: ( R_VectorSpace_of_LinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of X,Y)) by Th14, RSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( RealVectSpace (the carrier of X,Y)) by RLSUB_1: 10;

      reconsider h1 = h as VECTOR of ( RealVectSpace (the carrier of X,Y)) by A1, RLSUB_1: 10;

       A2:

      now

        assume

         A3: h = (a * f);

        let x be Element of X;

        h1 = (a * f1) by A1, A3, RLSUB_1: 14;

        hence (h9 . x) = (a * (f9 . x)) by Th2;

      end;

      now

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

        then h1 = (a * f1) by Th2;

        hence h = (a * f) by A1, RLSUB_1: 14;

      end;

      hence thesis by A2;

    end;

    theorem :: LOPBAN_1:18

    

     Th18: for X,Y be RealLinearSpace holds ( 0. ( R_VectorSpace_of_LinearOperators (X,Y))) = (the carrier of X --> ( 0. Y))

    proof

      let X,Y be RealLinearSpace;

      

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

      ( R_VectorSpace_of_LinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of X,Y)) by Th14, RSSPACE: 11;

      hence thesis by A1, RLSUB_1: 11;

    end;

    theorem :: LOPBAN_1:19

    

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

    proof

      let X,Y be RealLinearSpace;

      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, r be Real;

        

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

        .= (r * ( 0. Y))

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

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

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

      end;

      hence thesis by A1;

    end;

    begin

    theorem :: LOPBAN_1:20

    

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

    proof

      let X be RealNormSpace;

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

        reconsider k = m1 as Nat;

        take k;

        now

          let n be Nat;

          assume n >= k;

          then

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

           |.( ||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by NORMSP_1: 9;

          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, NORMSP_1: 23;

      hence thesis by A3, SEQ_2:def 7;

    end;

    definition

      let X,Y be RealNormSpace;

      let IT be LinearOperator of X, Y;

      :: LOPBAN_1:def8

      attr IT is Lipschitzian means

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

    end

    theorem :: LOPBAN_1:21

    

     Th21: for X,Y be RealNormSpace 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 RealNormSpace;

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

      end;

      take 0 ;

      thus thesis by A2;

    end;

    registration

      let X,Y be RealNormSpace;

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

        take f;

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

        hence thesis by Th21;

      end;

    end

    definition

      let X,Y be RealNormSpace;

      :: LOPBAN_1:def9

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

      : Def9: 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 ( R_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 Def6;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( R_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 RealNormSpace;

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

      coherence

      proof

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

        reconsider f as LinearOperator of X, Y by Th19;

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

        then f is Lipschitzian by Th21;

        hence thesis by Def9;

      end;

    end

    theorem :: LOPBAN_1:22

    

     Th22: for X,Y be RealNormSpace holds ( BoundedLinearOperators (X,Y)) is linearly-closed

    proof

      let X,Y be RealNormSpace;

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

      

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

      proof

        let v,u be VECTOR of ( R_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 Def6;

        f is Lipschitzian

        proof

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

          consider K2 be Real such that

           A4: 0 <= K2 and

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

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

          consider K1 be Real such that

           A6: 0 <= K1 and

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

          take K3 = (K1 + K2);

          now

            let x be VECTOR of X;

            

             A8: ||.((u1 . x) + (v1 . x)).|| <= ( ||.(u1 . x).|| + ||.(v1 . x).||) by NORMSP_1:def 1;

            

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

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

          end;

          hence thesis by A6, A4;

        end;

        hence thesis by Def9;

      end;

      for a be Real holds for v be VECTOR of ( R_VectorSpace_of_LinearOperators (X,Y)) st v in W holds (a * v) in W

      proof

        let a be Real;

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

         A11: v in W;

        reconsider f = (a * v) as LinearOperator of X, Y by Def6;

        f is Lipschitzian

        proof

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

          consider K be Real such that

           A12: 0 <= K and

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

          take ( |.a.| * K);

           A14:

          now

            let x be VECTOR of X;

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

            then

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

             ||.(a * (v1 . x)).|| = ( |.a.| * ||.(v1 . x).||) by NORMSP_1:def 1;

            hence ||.(f . x).|| <= (( |.a.| * K) * ||.x.||) by A15, Th17;

          end;

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

          hence thesis by A12, A14;

        end;

        hence thesis by Def9;

      end;

      hence thesis by A1, RLSUB_1:def 1;

    end;

    theorem :: LOPBAN_1:23

    for X,Y be RealNormSpace holds RLSStruct (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))) #) is Subspace of ( R_VectorSpace_of_LinearOperators (X,Y)) by Th22, RSSPACE: 11;

    registration

      let X,Y be RealNormSpace;

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

      coherence by Th22, RSSPACE: 11;

    end

    definition

      let X,Y be RealNormSpace;

      :: LOPBAN_1:def10

      func R_VectorSpace_of_BoundedLinearOperators (X,Y) -> RealLinearSpace equals RLSStruct (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))) #);

      coherence ;

    end

    registration

      let X,Y be RealNormSpace;

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

      coherence ;

    end

    registration

      let X,Y be RealNormSpace;

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

      coherence ;

    end

    definition

      let X,Y be RealNormSpace;

      let f be Element of ( R_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 Def9;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: LOPBAN_1:24

    

     Th24: for X,Y be RealNormSpace holds for f,g,h be VECTOR of ( R_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 RealNormSpace;

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

      

       A1: ( R_VectorSpace_of_BoundedLinearOperators (X,Y)) is Subspace of ( R_VectorSpace_of_LinearOperators (X,Y)) by Th22, RSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( R_VectorSpace_of_LinearOperators (X,Y)) by RLSUB_1: 10;

      reconsider h1 = h as VECTOR of ( R_VectorSpace_of_LinearOperators (X,Y)) by A1, RLSUB_1: 10;

      reconsider g1 = g as VECTOR of ( R_VectorSpace_of_LinearOperators (X,Y)) by A1, RLSUB_1: 10;

      hereby

        assume

         A2: h = (f + g);

        let x be Element of X;

        h1 = (f1 + g1) by A1, A2, RLSUB_1: 13;

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

      end;

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

      then h1 = (f1 + g1) by Th16;

      hence thesis by A1, RLSUB_1: 13;

    end;

    theorem :: LOPBAN_1:25

    

     Th25: for X,Y be RealNormSpace holds for f,h be VECTOR of ( R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds for a be Real holds h = (a * f) iff for x be VECTOR of X holds (h . x) = (a * (f . x))

    proof

      let X,Y be RealNormSpace;

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

      let a be Real;

      

       A1: ( R_VectorSpace_of_BoundedLinearOperators (X,Y)) is Subspace of ( R_VectorSpace_of_LinearOperators (X,Y)) by Th22, RSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( R_VectorSpace_of_LinearOperators (X,Y)) by RLSUB_1: 10;

      reconsider h1 = h as VECTOR of ( R_VectorSpace_of_LinearOperators (X,Y)) by A1, RLSUB_1: 10;

      hereby

        assume

         A2: h = (a * f);

        let x be Element of X;

        h1 = (a * f1) by A1, A2, RLSUB_1: 14;

        hence (h . x) = (a * (f . x)) by Th17;

      end;

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

      then h1 = (a * f1) by Th17;

      hence thesis by A1, RLSUB_1: 14;

    end;

    theorem :: LOPBAN_1:26

    

     Th26: for X,Y be RealNormSpace holds ( 0. ( R_VectorSpace_of_BoundedLinearOperators (X,Y))) = (the carrier of X --> ( 0. Y))

    proof

      let X,Y be RealNormSpace;

      

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

      ( R_VectorSpace_of_BoundedLinearOperators (X,Y)) is Subspace of ( R_VectorSpace_of_LinearOperators (X,Y)) by Th22, RSSPACE: 11;

      hence thesis by A1, RLSUB_1: 11;

    end;

    definition

      let X,Y be RealNormSpace;

      let f be object;

      :: LOPBAN_1:def11

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

      : Def11: f;

      coherence by A1, Def9;

    end

    definition

      let X,Y be RealNormSpace;

      let u be LinearOperator of X, Y;

      :: LOPBAN_1:def12

      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 ;

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

    

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

    proof

      let X,Y be RealNormSpace;

      let g be Lipschitzian LinearOperator of X, Y;

      consider K be Real such that

       A1: 0 <= K and

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

      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;

    theorem :: LOPBAN_1:28

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

    proof

      let X,Y be RealNormSpace;

      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 ;

              (g . t) = (g . ( 0 * ( 0. X))) by A3

              .= ( 0 * (g . ( 0. X))) by Def5

              .= ( 0. Y) by RLVECT_1: 10;

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

            end;

              case

               A5: t <> ( 0. X);

              reconsider t1 = (( ||.t.|| " ) * t) as VECTOR of X;

              

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

              

               A7: (( ||.(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).||;

              

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

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

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

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

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

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

               ||.t1.|| = ( |.( ||.t.|| " ).| * ||.t.||) by NORMSP_1:def 1

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

              then

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

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

              .= ||.(( ||.t.|| " ) * (g . t)).|| by A8, NORMSP_1:def 1

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

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

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

            end;

          end;

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

        end;

        take K;

         0 <= K

        proof

          consider r0 be object such that

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

          reconsider r0 as Real by A10;

          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;

          end;

          then 0 <= r0 by A10;

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

        end;

        hence g is Lipschitzian by A2;

      end;

      hence thesis by Th27;

    end;

    definition

      let X,Y be RealNormSpace;

      :: LOPBAN_1:def13

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

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

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

      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 :: LOPBAN_1:29

    

     Th29: for X,Y be RealNormSpace holds for f be Lipschitzian LinearOperator of X, Y holds ( modetrans (f,X,Y)) = f

    proof

      let X,Y be RealNormSpace;

      let f be Lipschitzian LinearOperator of X, Y;

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

      hence thesis by Def11;

    end;

    theorem :: LOPBAN_1:30

    

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

    proof

      let X,Y be RealNormSpace;

      let f be Lipschitzian LinearOperator of X, Y;

      reconsider f9 = f as set;

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

      

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

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

    end;

    definition

      let X,Y be RealNormSpace;

      :: LOPBAN_1:def14

      func R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty NORMSTR equals NORMSTR (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( BoundedLinearOperatorsNorm (X,Y)) #);

      coherence ;

    end

    theorem :: LOPBAN_1:31

    

     Th31: for X,Y be RealNormSpace holds (the carrier of X --> ( 0. Y)) = ( 0. ( R_NormSpace_of_BoundedLinearOperators (X,Y)))

    proof

      let X,Y be RealNormSpace;

      (the carrier of X --> ( 0. Y)) = ( 0. ( R_VectorSpace_of_BoundedLinearOperators (X,Y))) by Th26

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

      hence thesis;

    end;

    theorem :: LOPBAN_1:32

    

     Th32: for X,Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds for 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 RealNormSpace;

      let f be Point of ( R_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 Th27;

      now

        let t be VECTOR of X;

        now

          per cases ;

            case

             A3: t = ( 0. X);

            then

             A4: ||.t.|| = 0 ;

            (g . t) = (g . ( 0 * ( 0. X))) by A3

            .= ( 0 * (g . ( 0. X))) by Def5

            .= ( 0. Y) by RLVECT_1: 10;

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

          end;

            case

             A5: t <> ( 0. X);

            reconsider t1 = (( ||.t.|| " ) * t) as VECTOR of X;

            

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

            

             A7: |.( ||.t.|| " ).| = |.(1 * ( ||.t.|| " )).|

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

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

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

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

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

            

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

            .= ||.(( ||.t.|| " ) * (g . t)).|| by A7, NORMSP_1:def 1

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

             ||.t1.|| = ( |.( ||.t.|| " ).| * ||.t.||) by NORMSP_1:def 1

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

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

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

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

            then

             A9: ( ||.(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 A9, XREAL_1: 64;

          end;

        end;

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

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_1:33

    

     Th33: for X,Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||

    proof

      let X,Y be RealNormSpace;

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

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

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

      

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

      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;

      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 :: LOPBAN_1:34

    

     Th34: for X,Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = ( 0. ( R_NormSpace_of_BoundedLinearOperators (X,Y))) holds 0 = ||.f.||

    proof

      let X,Y be RealNormSpace;

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

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

      thus ||.f.|| = 0

      proof

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

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

        

         A5: z = g by A1, Th31;

         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 ;

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

        hence thesis;

      end;

    end;

    registration

      let X,Y be RealNormSpace;

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

      coherence ;

    end

    definition

      let X,Y be RealNormSpace;

      let f be Element of ( R_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 Def9;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: LOPBAN_1:35

    

     Th35: for X,Y be RealNormSpace holds for f,g,h be Point of ( R_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 RealNormSpace;

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

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

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

      hence thesis by Th24;

    end;

    theorem :: LOPBAN_1:36

    

     Th36: for X,Y be RealNormSpace holds for f,h be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds for a be Real holds h = (a * f) iff for x be VECTOR of X holds (h . x) = (a * (f . x))

    proof

      let X,Y be RealNormSpace;

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

      let a be Real;

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

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

      h = (a * f) iff h1 = (a * f1);

      hence thesis by Th25;

    end;

    theorem :: LOPBAN_1:37

    

     Th37: for X be RealNormSpace holds for Y be RealNormSpace holds for f,g be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds for a be Real holds ( ||.f.|| = 0 iff f = ( 0. ( R_NormSpace_of_BoundedLinearOperators (X,Y)))) & ||.(a * f).|| = ( |.a.| * ||.f.||) & ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

    proof

      let X be RealNormSpace;

      let Y be RealNormSpace;

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

      let a be Real;

       A1:

      now

        assume

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

        thus ||.f.|| = 0

        proof

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

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

          

           A6: z = g by A2, Th31;

           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 ;

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

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

        

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

          then

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

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

          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 NORMSP_1:def 1;

          

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

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

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

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

        hence thesis by A18, A10;

      end;

      

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

      proof

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

        

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

         A21:

        now

          

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

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

          then

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

          

           A25: ||.(a * (f1 . t)).|| = ( |.a.| * ||.(f1 . t).||) by NORMSP_1:def 1;

          

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

           ||.(h1 . t).|| = ||.(a * (f1 . t)).|| by Th36;

          hence ||.(h1 . t).|| <= ( |.a.| * ||.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 <= ( |.a.| * ||.f.||) by A21;

        end;

         A28:

        now

          per cases ;

            case

             A29: a <> 0 ;

             A30:

            now

              

               A31: 0 <= ||.(a * f).|| by Th33;

              let t be VECTOR of X;

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

              then

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

               ||.(h1 . t).|| <= ( ||.(a * f).|| * ||.t.||) by Th32;

              then

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

              (h1 . t) = (a * (f1 . t)) by Th36;

              

              then

               A34: ((a " ) * (h1 . t)) = (((a " ) * a) * (f1 . t)) by RLVECT_1:def 7

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

              .= (f1 . t) by RLVECT_1:def 8;

              

               A35: |.(a " ).| = |.(1 * (a " )).|

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

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

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

              .= ( |.a.| " );

              

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

               ||.((a " ) * (h1 . t)).|| = ( |.(a " ).| * ||.(h1 . t).||) by NORMSP_1:def 1;

              hence ||.(f1 . t).|| <= (( |.a.| " ) * ||.(a * 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 <= (( |.a.| " ) * ||.(a * f).||) by A30;

            end;

            

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

            

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

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

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

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

            then

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

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

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

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

          end;

            case

             A41: a = 0 ;

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

            

             A42: (a * f) = (a * fz)

            .= ( 0. ( R_VectorSpace_of_BoundedLinearOperators (X,Y))) by A41, RLVECT_1: 10

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

            

            thus ( |.a.| * ||.f.||) = ( 0 * ||.f.||) by A41, ABSVALUE: 2

            .= ||.(a * f).|| by A42, Th34;

          end;

        end;

        (( BoundedLinearOperatorsNorm (X,Y)) . (a * f)) = ( upper_bound ( PreNorms h1)) by Th30;

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

        hence thesis by A28, XXREAL_0: 1;

      end;

      now

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

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

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

        assume

         A43: ||.f.|| = 0 ;

        now

          let t be VECTOR of X;

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

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

          

          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. ( R_NormSpace_of_BoundedLinearOperators (X,Y))) by Th31;

      end;

      hence thesis by A1, A19, A9;

    end;

    theorem :: LOPBAN_1:38

    

     Th38: for X,Y be RealNormSpace holds ( R_NormSpace_of_BoundedLinearOperators (X,Y)) is reflexive discerning RealNormSpace-like

    proof

      let X,Y be RealNormSpace;

      thus ||.( 0. ( R_NormSpace_of_BoundedLinearOperators (X,Y))).|| = 0 by Th37;

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

      hence thesis by NORMSP_1:def 1;

    end;

    theorem :: LOPBAN_1:39

    

     Th39: for X,Y be RealNormSpace holds ( R_NormSpace_of_BoundedLinearOperators (X,Y)) is RealNormSpace

    proof

      let X,Y be RealNormSpace;

       RLSStruct (# ( BoundedLinearOperators (X,Y)), ( Zero_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Add_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))), ( Mult_ (( BoundedLinearOperators (X,Y)),( R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace;

      hence thesis by Th38, RSSPACE3: 2;

    end;

    registration

      let X,Y be RealNormSpace;

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

      coherence by Th39;

    end

    theorem :: LOPBAN_1:40

    

     Th40: for X,Y be RealNormSpace holds for f,g,h be Point of ( R_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 RealNormSpace;

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

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

      hereby

        assume h = (f - g);

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

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

        then

         A1: (h + g) = f;

        now

          let x be VECTOR of X;

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

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

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

      end;

      then f = (h + g) by Th35;

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

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

      hence thesis;

    end;

    begin

    definition

      let X be RealNormSpace;

      :: LOPBAN_1:def15

      attr X is complete means

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

    end

    registration

      cluster complete for RealNormSpace;

      existence by Def15, RSSPACE3: 9;

    end

    definition

      mode RealBanachSpace is complete RealNormSpace;

    end

    

     Lm3: 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 ee = 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 :: LOPBAN_1:41

    

     Th41: for X be RealNormSpace holds for seq be sequence of X st seq is convergent holds ||.seq.|| is convergent & ( lim ||.seq.||) = ||.( lim seq).||

    proof

      let X be RealNormSpace;

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

        reconsider k as Nat;

        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 NORMSP_1: 9;

          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 :: LOPBAN_1:42

    

     Th42: for X,Y be RealNormSpace st Y is complete holds for seq be sequence of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent

    proof

      let X,Y be RealNormSpace such that

       A1: Y is complete;

      let vseq be sequence of ( R_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;

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

          k in NAT by ORDINAL1:def 12;

          then

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

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

          then

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

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

          then

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

          m in NAT by ORDINAL1:def 12;

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

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

          hence thesis by Th32;

        end;

        now

          let e be Real such that

           A10: e > 0 ;

          now

            per cases ;

              case

               A11: x = ( 0. X);

              reconsider k = 0 as Nat;

              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 n >= k and m >= k;

                m in NAT by ORDINAL1:def 12;

                

                then

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

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

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

                .= ( 0. Y) by RLVECT_1: 10;

                n in NAT by ORDINAL1:def 12;

                

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

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

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

                .= ( 0. Y) by RLVECT_1: 10;

                

                then ||.((xseq . n) - (xseq . m)).|| = ||.( 0. Y).|| by A12

                .= 0 ;

                hence thesis by A10;

              end;

            end;

              case x <> ( 0. X);

              then

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

              then

               A14: ||.x.|| > 0 ;

              then (e / ||.x.||) > 0 by A10, XREAL_1: 139;

              then

              consider k be Nat such that

               A15: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < (e / ||.x.||) by A2, RSSPACE3: 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

                 A16: n >= k and

                 A17: m >= k;

                 ||.((vseq . n) - (vseq . m)).|| < (e / ||.x.||) by A15, A16, A17;

                then

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

                

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

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

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

                .= e;

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

                hence thesis by A18, A19, 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 RSSPACE3: 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

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

       A21:

      now

        let x,y be VECTOR of X;

        consider xseq be sequence of Y such that

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

         A23: xseq is convergent and

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

        consider zseq be sequence of Y such that

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

         A26: (tseq . (x + y)) = ( lim zseq) by A20;

        consider yseq be sequence of Y such that

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

         A28: yseq is convergent and

         A29: (tseq . y) = ( lim yseq) by A20;

        now

          let n be Nat;

          

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

          .= ((( 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 A22

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

        end;

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

        hence (tseq . (x + y)) = ((tseq . x) + (tseq . y)) by A23, A24, A28, A29, A26, NORMSP_1: 25;

      end;

      now

        let x be VECTOR of X;

        let a be Real;

        consider xseq be sequence of Y such that

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

         A31: xseq is convergent and

         A32: (tseq . x) = ( lim xseq) by A20;

        consider zseq be sequence of Y such that

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

         A34: (tseq . (a * x)) = ( lim zseq) by A20;

        now

          let n be Nat;

          

          thus (zseq . n) = (( modetrans ((vseq . n),X,Y)) . (a * x)) by A33

          .= (a * (( modetrans ((vseq . n),X,Y)) . x)) by Def5

          .= (a * (xseq . n)) by A30;

        end;

        then zseq = (a * xseq) by NORMSP_1:def 5;

        hence (tseq . (a * x)) = (a * (tseq . x)) by A31, A32, A34, NORMSP_1: 28;

      end;

      then

      reconsider tseq as LinearOperator of X, Y by A21, Def5, VECTSP_1:def 20;

      now

        let e1 be Real such that

         A35: e1 > 0 ;

        reconsider e = e1 as Real;

        consider k be Nat such that

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

        reconsider k as Nat;

        take k;

        now

          let m be Nat;

          assume m >= k;

          then

           A37: ||.((vseq . m) - (vseq . k)).|| < e by A36;

          

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

          

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

           |.( ||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| by NORMSP_1: 9;

          hence |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1 by A39, A38, A37, XXREAL_0: 2;

        end;

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

      end;

      then

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

      

       A41: tseq is Lipschitzian

      proof

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

         A42:

        now

          let x be VECTOR of X;

          consider xseq be sequence of Y such that

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

           A44: xseq is convergent and

           A45: (tseq . x) = ( lim xseq) by A20;

          

           A46: ||.(tseq . x).|| = ( lim ||.xseq.||) by A44, A45, Th20;

          

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

          proof

            let m be Nat;

            

             A48: (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A43;

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

            hence thesis by A48, Th29, Th32;

          end;

          

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

          proof

            let n be Nat;

            

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

            

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

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

            hence thesis by A50, A51, SEQ_1: 9;

          end;

          

           A52: ( ||.x.|| (#) ||.vseq.||) is convergent by A40;

          

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

           ||.xseq.|| is convergent by A44, A45, Th20;

          hence ||.(tseq . x).|| <= (( lim ||.vseq.||) * ||.x.||) by A46, A49, A52, A53, SEQ_2: 18;

        end;

        now

          let n be Nat;

           ||.(vseq . n).|| >= 0 ;

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

        end;

        hence thesis by A40, A42, SEQ_2: 17;

      end;

      

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

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

        take k;

        now

          let n be Nat such that

           A56: n >= k;

          now

            let x be VECTOR of X;

            consider xseq be sequence of Y such that

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

             A58: xseq is convergent and

             A59: (tseq . x) = ( lim xseq) by A20;

            

             A60: 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 Def9;

              

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

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

              then

               A62: ( modetrans ((vseq . m),X,Y)) = (vseq . m) by Th29;

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

              then

               A63: ( modetrans ((vseq . k),X,Y)) = (vseq . k) by Th29;

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

              then ((xseq . m) - (xseq . k)) = (h1 . x) by A62, A63, A61, Th40;

              hence thesis by Th32;

            end;

            

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

            proof

              let m be Nat;

              assume m >= k;

              then

               A65: ||.((vseq . n) - (vseq . m)).|| < e by A55, A56;

              

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

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

              hence thesis by A66, 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

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

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

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

              end;

              then

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

              

               A69: (xseq - (xseq . n)) is convergent by A58, NORMSP_1: 21;

              ( lim (xseq - (xseq . n))) = ((tseq . x) - (xseq . n)) by A58, A59, NORMSP_1: 27;

              then

               A70: ( lim rseq) = ||.((tseq . x) - (xseq . n)).|| by A69, A68, Th41;

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

              proof

                let m be Nat such that

                 A71: m >= k;

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

                .= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1: 7;

                hence thesis by A64, A71;

              end;

              then ( lim rseq) <= (e * ||.x.||) by A69, A68, Lm3, Th41;

              hence thesis by A70, NORMSP_1: 7;

            end;

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

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

      reconsider tv = tseq as Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by Def9;

      

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

         A73: e > 0 ;

        consider k be Nat such that

         A74: 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 A54, A73;

        now

          set g1 = tseq;

          let n be Nat such that

           A75: n >= k;

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

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

           A76:

          now

            let t be VECTOR of X;

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

            then

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

            

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

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

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

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

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

          end;

           A79:

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

          end;

          

           A80: (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 Th30;

          hence ||.((vseq . n) - tv).|| <= e by A79, A80;

        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

         A81: e > 0 ;

        consider m be Nat such that

         A82: for n be Nat st n >= m holds ||.((vseq . n) - tv).|| <= (e / 2) by A72, A81, XREAL_1: 215;

        

         A83: (e / 2) < e by A81, XREAL_1: 216;

        now

          let n be Nat;

          assume n >= m;

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

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

        end;

        hence thesis;

      end;

      hence thesis by NORMSP_1:def 6;

    end;

    theorem :: LOPBAN_1:43

    

     Th43: for X be RealNormSpace holds for Y be RealBanachSpace holds ( R_NormSpace_of_BoundedLinearOperators (X,Y)) is RealBanachSpace

    proof

      let X be RealNormSpace;

      let Y be RealBanachSpace;

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

      hence thesis by Def15;

    end;

    registration

      let X be RealNormSpace;

      let Y be RealBanachSpace;

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

      coherence by Th43;

    end