text:
:: Complex {B}anach Space of Bounded Linear Operators
::  by Noboru Endou

environ

 vocabularies NUMBERS, XBOOLE_0, FUNCT_1, ZFMISC_1, XCMPLX_0, FUNCOP_1,
      SUBSET_1, FUNCT_2, RELAT_1, PARTFUN1, CLVECT_1, STRUCT_0, RLVECT_1,
      LOPBAN_1, SUPINF_2, ARYTM_3, ARYTM_1, COMPLEX1, ALGSTR_0, MONOID_0,
      TARSKI, MSSUBFAM, UNIALG_1, RLSUB_1, RSSPACE, NAT_1, PRE_TOPC, SEQ_2,
      ORDINAL2, NORMSP_1, XXREAL_0, CARD_1, REAL_1, XXREAL_2, SEQ_4, REWRITE1,
      RSSPACE3, SEQ_1, VALUED_1, CLOPBAN1, METRIC_1, RELAT_2, FCONT_1,
      ASYMPT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, FUNCT_3, PRE_TOPC, DOMAIN_1, FUNCOP_1, BINOP_1, XCMPLX_0,
      XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0,
      ALGSTR_0, MONOID_0, NUMBERS, RLVECT_1, NORMSP_0, NORMSP_1, VALUED_1,
      SEQ_1, SEQ_2, SEQ_4, FUNCSDOM, CLVECT_1, CSSPACE, CSSPACE3, LOPBAN_1,
      VECTSP_1;
 constructors DOMAIN_1, REAL_1, COMPLEX1, FUNCSDOM, MONOID_0, LOPBAN_1,
      CSSPACE3, SEQ_4, RELSET_1, BINOP_2, SEQ_2, COMSEQ_2, FUNCT_3, SEQ_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
      XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, MONOID_0, CLVECT_1,
      CSSPACE3, VALUED_1, VALUED_0, SEQ_4, FUNCT_1, NAT_1, SEQ_1, SEQ_2;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions FUNCT_1, ALGSTR_0, VECTSP_1, XXREAL_2;
 equalities BINOP_1, STRUCT_0, ALGSTR_0, NORMSP_0;
 expansions FUNCT_1, BINOP_1, NORMSP_0;
 theorems ALGSTR_0, XBOOLE_0, TARSKI, ABSVALUE, RLVECT_1, FUNCOP_1, XREAL_0,
      XCMPLX_0, SEQ_1, SEQ_2, FUNCT_1, NAT_1, FUNCT_2, SEQ_4, FUNCT_3,
      CLVECT_1, LOPBAN_1, CSSPACE, COMPLEX1, CSSPACE3, MONOID_0, XREAL_1,
      XXREAL_0, NORMSP_1, VECTSP_1, NORMSP_0, ORDINAL1;
 schemes SEQ_1, FUNCT_2, XBOOLE_0, BINOP_1;

begin :: Complex Vector Space of Operators

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;
  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;
  func FuncExtMult(X,Y) -> Function of [:COMPLEX,Funcs(X,the carrier of Y):],
  Funcs(X,the carrier of Y) means
  :Def1:
  for c being Complex, f being Element of
  Funcs(X,the carrier of Y), x being 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 being 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 being 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 being Complex, f being Element of Funcs(X,the carrier of Y),
    x being Element of X holds (it1.[c,f]).x = c*(f.x) and
A4: for c being Complex, f being Element of Funcs(X,the carrier of Y),
    x being 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 Th1:
  for x being 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 Th2:
  h = (FuncExtMult(X,Y)).[a,f] iff for x being Element of X holds h
  .x = a*(f.x)
proof
  thus h = (FuncExtMult(X,Y)).[a,f] implies for x being 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 being Element of X holds h.x = a*(f.x);
    for x being 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 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 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 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 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 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 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 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 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,def 3
,def 4,def 5,RLVECT_1:def 2,def 3,def 4;
end;

definition
  let X be non empty set;
  let Y be ComplexLinearSpace;
  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;
  redefine func f.x -> VECTOR of Y;
  coherence
  proof
    consider g being 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
  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 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 :: Complex Vector Space of Linear Operators

definition
  let X, Y be non empty CLSStruct;
  let IT be Function of X,Y;
  attr IT is homogeneous means
  :Def3:
  for x being VECTOR of X, r being 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;
  func LinearOperators(X,Y) -> Subset of ComplexVectSpace(the carrier of X, Y)
  means
  :Def4:
  for x being 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 being set such that
A1: for x being 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 being set holds x in X1 iff x is LinearOperator of X,Y and
A4: for x being set holds x in X2 iff x is LinearOperator of X,Y;
    for x being 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 being 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 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 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
  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;
  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;
  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 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 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 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 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 :: Complex Normed Linear Space of Bounded Linear Operators

theorem 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;
  attr IT is Lipschitzian means
  :Def6:
  ex K being Real st 0 <= K &
  for x being VECTOR of X holds ||. IT.x .|| <= K * ||. x .||;
end;

theorem 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;
  func BoundedLinearOperators(X,Y) -> Subset of
  C_VectorSpace_of_LinearOperators(X,Y) means
  :Def7:
  for x being 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 being set such that
A1: for x being 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 being set holds x in X1 iff x is Lipschitzian LinearOperator of X,Y
    and
A4: for x being set holds x in X2 iff x is Lipschitzian LinearOperator of X,Y;
    for x being 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 being 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 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
  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;
  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;
  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 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 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 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 such that
A1: f in BoundedLinearOperators(X,Y);
  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;
  func PreNorms(u) -> non empty Subset of REAL equals
  {||.u.t.|| where t is
  VECTOR of X : ||.t.|| <= 1 };
  coherence
  proof
A1: now
      let x be object;
      now
        assume x in {||.u.t.|| where t is 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 is 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 is VECTOR of X : ||.t.|| <= 1 };
    hence thesis by A1,TARSKI:def 3;
  end;
end;

theorem 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
  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;
  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 being Function of BoundedLinearOperators(X,Y),REAL st
for x being 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 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 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;
  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 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 Th31:
  for X,Y be ComplexNormSpace,
  f being 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 being 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 is 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 Th32:
  for X,Y be ComplexNormSpace, f being Point of
  C_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 <= ||.f.||
proof
  let X,Y be ComplexNormSpace;
  let f being 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 Th33:
  for X,Y be ComplexNormSpace, f being 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 being 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;
  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 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 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 Th36:
  for X,Y be ComplexNormSpace, f, g being 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 being 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 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 being Point of C_NormSpace_of_BoundedLinearOperators(X,Y) 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 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 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 :: Complex Banach Space of Bounded Linear Operators

definition
  let X be ComplexNormSpace;
  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 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 Th41:
  for X,Y be ComplexNormSpace st Y is complete 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 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 ex k be Nat st
  for n be Nat st n >= k
   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 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 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 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;

subset_name: curated


TITLE: Monoids of endomorphisms of nonisomorphic groups
QUESTION [17 upvotes]: Can monoids of endomorphisms of nonisomorphic groups be isomorphic ?

REPLY [15 votes]: It is proved in $[$1$]$ that the tetrahedral group $A_4$ of order $12$ and the binary tetrahedral group of order $24$ have isomorphic endomorphism monoids.  So this gives a finite example.  It is also the smallest order example.  Moreover, no other finite groups have isomorphic endomorphism monoid to the endomorphism monoid of these two groups without being isomorphic to one of them.
$[$1$]$ P. Puusemp, Groups of order 24 and their endomorphism semigroups, J. Math. Sci. (2007) 144(2) 3980–3992
(link at Springerlink).


TITLE: What is the Laurent Series for $\frac{1}{z^2}$ around z=0?
QUESTION [1 upvotes]: How do I get the Laurent Series of $\frac{1}{z^2}$ around $z=0$ ?

REPLY [3 votes]: You already have it: $\frac1{z^2}$


TITLE: Tangent plane to a surface at a point
QUESTION [0 upvotes]: We have a function $f(x,y) = x \sin(xy) + 2$. The equation for the tangent plane to the function $f: \mathbb{R}^2 \to \mathbb{R}$ at the point $(a,b)$ is given by $$z = f(a,b) + f_x(a,b)(x-a) + f_y(a,b)(y-b)$$
So let's say our point is $(\pi, 1)$. I can mostly simply use the equation above but for $f_x$ the partial derivative is messy. Wolfram alpha says it is $x(x y'(x) +y)\cos(xy)+\sin(xy)$. How should you deal with the $y'(x)$ term? For the other $x$ and $y$ you simply plug in the coordinates of the point, but with the $y'(x)$ term I'm stumped. Perhaps there is a different form of the derivative?

REPLY [1 votes]: Wolfram Alpha is assuming that $y$ is a function of $x$. Here, it isn't; it's independent of $x$. That means you can substitute $y'(x)=0$.
Another neat trick: If you want to find $f_x(a,b)$, you can take the derivative of $f(x,b)$ with respect to $x$, then substitute $x=a$. A similar trick works for $f_y(a,b)$.