CLOPBAN1: Complex {B}anach Space of Bounded Linear Operators

:: Complex {B}anach Space of Bounded Linear Operators
:: by Noboru Endou
::
:: Received February 24, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users

begin

definition

let X be set ;
let Y be non empty set ;
let F be Function of [:COMPLEX,Y:],Y;
let c be complex number ;
let f be Function of X,Y;
:: original: [;]
redefine func F [;] (c,f) -> Element of Funcs (X,Y);
coherence

proof end;

end;

theorem Th1: :: CLOPBAN1:1

for X being non empty set
for Y being ComplexLinearSpace ex MULT being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for s being Element of X holds (MULT . [c,f]) . s = c * (f . s)

proof 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: :: CLOPBAN1:def 1
for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it . [c,f]) . x = c * (f . x);
existence by Th1;
uniqueness

proof end;

end;

:: deftheorem Def1 defines FuncExtMult CLOPBAN1:def 1 :

theorem Th2: :: CLOPBAN1:2

for X being non empty set
for Y being ComplexLinearSpace
for x being Element of X holds (FuncZero (X,Y)) . x = 0. Y

proof end;

theorem Th3: :: CLOPBAN1:3

for X being non empty set
for Y being ComplexLinearSpace
for h, f being Element of Funcs (X, the carrier of Y)
for a being Complex holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )

proof end;

theorem Th4: :: CLOPBAN1:4

for X being non empty set
for Y being ComplexLinearSpace
for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)

proof end;

theorem Th5: :: CLOPBAN1:5

for X being non empty set
for Y being ComplexLinearSpace
for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)

proof end;

theorem Th6: :: CLOPBAN1:6

for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f

proof end;

theorem Th7: :: CLOPBAN1:7

for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)

proof end;

theorem Th8: :: CLOPBAN1:8

for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1r,f] = f

proof end;

theorem Th9: :: CLOPBAN1:9

for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

proof end;

theorem Th10: :: CLOPBAN1:10

for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]

proof end;

Lm1: for X being non empty set
for Y being ComplexLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]

proof end;

theorem Th11: :: CLOPBAN1:11

for X being non empty set
for Y being ComplexLinearSpace holds CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace

proof end;

definition

let X be non empty set ;
let Y be ComplexLinearSpace;
func ComplexVectSpace (X,Y) -> ComplexLinearSpace equals :: CLOPBAN1:def 2
CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);
coherence by Th11;

end;

:: deftheorem defines ComplexVectSpace CLOPBAN1:def 2 :

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

end;

definition

let X be non empty set ;
let Y be ComplexLinearSpace;
let f be VECTOR of (ComplexVectSpace (X,Y));
let x be Element of X;
:: original: .
redefine func f . x -> VECTOR of Y;
coherence

proof end;

end;

theorem :: CLOPBAN1:12

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

theorem Th13: :: CLOPBAN1:13

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

proof end;

begin

definition

let X, Y be non empty CLSStruct ;
let IT be Function of X,Y;
canceled;
attr IT is homogeneous means :Def4: :: CLOPBAN1:def 4
for x being VECTOR of X
for r being Complex holds IT . (r * x) = r * (IT . x);

end;

:: deftheorem CLOPBAN1:def 3 :

:: deftheorem Def4 defines homogeneous CLOPBAN1:def 4 :

registration

let X be non empty CLSStruct ;
let Y be ComplexLinearSpace;
cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous Element of bool [: the carrier of X, the carrier of Y:];
existence

proof 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 :Def5: :: CLOPBAN1:def 5
for x being set holds
( x in it iff x is LinearOperator of X,Y );
existence

proof end;

proof end;

end;

:: deftheorem Def5 defines LinearOperators CLOPBAN1:def 5 :

registration

let X, Y be ComplexLinearSpace;
cluster LinearOperators (X,Y) -> non empty functional ;
coherence

proof end;

end;

theorem :: CLOPBAN1:14

canceled;

theorem Th15: :: CLOPBAN1:15

for X, Y being ComplexLinearSpace holds LinearOperators (X,Y) is linearly-closed

proof end;

theorem :: CLOPBAN1:16

for X, Y being 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 Th15, CSSPACE:13;

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)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence by Th15, CSSPACE:13;

end;

definition

let X, Y be ComplexLinearSpace;
func C_VectorSpace_of_LinearOperators (X,Y) -> ComplexLinearSpace equals :: CLOPBAN1:def 6
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;

:: deftheorem defines C_VectorSpace_of_LinearOperators CLOPBAN1:def 6 :

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

end;

definition

let X, Y be ComplexLinearSpace;
let f be Element of (C_VectorSpace_of_LinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence

proof end;

end;

theorem :: CLOPBAN1:17

canceled;

theorem Th18: :: CLOPBAN1:18

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

proof end;

theorem Th19: :: CLOPBAN1:19

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

proof end;

theorem Th20: :: CLOPBAN1:20

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

proof end;

theorem Th21: :: CLOPBAN1:21

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

proof end;

begin

theorem Th22: :: CLOPBAN1:22

for X being ComplexNormSpace
for seq being sequence of X
for g being Point of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )

proof end;

definition

let X, Y be ComplexNormSpace;
let IT be LinearOperator of X,Y;
attr IT is bounded means :Def7: :: CLOPBAN1:def 7
ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) );

end;

:: deftheorem Def7 defines bounded CLOPBAN1:def 7 :

theorem Th23: :: CLOPBAN1:23

for X, Y being ComplexNormSpace
for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds
f is bounded

proof end;

registration

let X, Y be ComplexNormSpace;
cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous bounded Element of bool [: the carrier of X, the carrier of Y:];
existence

proof end;

end;

definition

let X, Y be ComplexNormSpace;
func BoundedLinearOperators (X,Y) -> Subset of (C_VectorSpace_of_LinearOperators (X,Y)) means :Def8: :: CLOPBAN1:def 8
for x being set holds
( x in it iff x is bounded LinearOperator of X,Y );
existence

proof end;

proof end;

end;

:: deftheorem Def8 defines BoundedLinearOperators CLOPBAN1:def 8 :

registration

let X, Y be ComplexNormSpace;
cluster BoundedLinearOperators (X,Y) -> non empty ;
coherence

proof end;

end;

theorem Th24: :: CLOPBAN1:24

for X, Y being ComplexNormSpace holds BoundedLinearOperators (X,Y) is linearly-closed

proof end;

theorem :: CLOPBAN1:25

for X, Y being 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 Th24, CSSPACE:13;

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)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence by Th24, CSSPACE:13;

end;

definition

let X, Y be ComplexNormSpace;
func C_VectorSpace_of_BoundedLinearOperators (X,Y) -> ComplexLinearSpace equals :: CLOPBAN1:def 9
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;

:: deftheorem defines C_VectorSpace_of_BoundedLinearOperators CLOPBAN1:def 9 :

registration

let X, Y be ComplexNormSpace;
cluster C_VectorSpace_of_BoundedLinearOperators (X,Y) -> strict ;
coherence ;

end;

registration

let X, Y be ComplexNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (C_VectorSpace_of_BoundedLinearOperators (X,Y));
coherence ;

end;

definition

let X, Y be ComplexNormSpace;
let f be Element of (C_VectorSpace_of_BoundedLinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence

proof end;

end;

theorem :: CLOPBAN1:26

canceled;

theorem Th27: :: CLOPBAN1:27

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

proof end;

theorem Th28: :: CLOPBAN1:28

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

proof end;

theorem Th29: :: CLOPBAN1:29

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

proof end;

definition

let X, Y be ComplexNormSpace;
let f be set ;
assume A1: f in BoundedLinearOperators (X,Y) ;
func modetrans (f,X,Y) -> bounded LinearOperator of X,Y equals :Def10: :: CLOPBAN1:def 10
f;
coherence by A1, Def8;

end;

:: deftheorem Def10 defines modetrans CLOPBAN1:def 10 :

definition

let X, Y be ComplexNormSpace;
let u be LinearOperator of X,Y;
func PreNorms u -> non empty Subset of REAL equals :: CLOPBAN1:def 11
{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;
coherence

proof end;

end;

:: deftheorem defines PreNorms CLOPBAN1:def 11 :

theorem Th30: :: CLOPBAN1:30

for X, Y being ComplexNormSpace
for g being bounded LinearOperator of X,Y holds PreNorms g is bounded_above

proof end;

theorem :: CLOPBAN1:31

for X, Y being ComplexNormSpace
for g being LinearOperator of X,Y holds
( g is bounded iff PreNorms g is bounded_above )

proof end;

theorem Th32: :: CLOPBAN1:32

for X, Y being ComplexNormSpace ex NORM being Function of (BoundedLinearOperators (X,Y)),REAL st
for f being set st f in BoundedLinearOperators (X,Y) holds
NORM . f = upper_bound (PreNorms (modetrans (f,X,Y)))

proof end;

definition

let X, Y be ComplexNormSpace;
func BoundedLinearOperatorsNorm (X,Y) -> Function of (BoundedLinearOperators (X,Y)),REAL means :Def12: :: CLOPBAN1:def 12
for x being set st x in BoundedLinearOperators (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));
existence by Th32;
uniqueness

proof end;

end;

:: deftheorem Def12 defines BoundedLinearOperatorsNorm CLOPBAN1:def 12 :

theorem Th33: :: CLOPBAN1:33

for X, Y being ComplexNormSpace
for f being bounded LinearOperator of X,Y holds modetrans (f,X,Y) = f

proof end;

theorem Th34: :: CLOPBAN1:34

for X, Y being ComplexNormSpace
for f being bounded LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)

proof end;

definition

let X, Y be ComplexNormSpace;
func C_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty CNORMSTR equals :: CLOPBAN1:def 13
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;

:: deftheorem defines C_NormSpace_of_BoundedLinearOperators CLOPBAN1:def 13 :

theorem Th35: :: CLOPBAN1:35

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

proof end;

theorem Th36: :: CLOPBAN1:36

for X, Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))
for g being bounded LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

proof end;

theorem Th37: :: CLOPBAN1:37

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

proof end;

theorem Th38: :: CLOPBAN1:38

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

proof end;

registration

let X, Y be ComplexNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (C_NormSpace_of_BoundedLinearOperators (X,Y));
coherence ;

end;

definition

let X, Y be ComplexNormSpace;
let f be Element of (C_NormSpace_of_BoundedLinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence

proof end;

end;

theorem Th39: :: CLOPBAN1:39

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

proof end;

theorem Th40: :: CLOPBAN1:40

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

proof end;

theorem Th41: :: CLOPBAN1:41

for X, Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

proof end;

theorem Th42: :: CLOPBAN1:42

for X, Y being ComplexNormSpace holds
( C_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like )

proof end;

theorem Th43: :: CLOPBAN1:43

for X, Y being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace

proof end;

registration

let X, Y be ComplexNormSpace;
cluster C_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence by Th43;

end;

theorem Th44: :: CLOPBAN1:44

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

proof end;

begin

definition

let X be ComplexNormSpace;
attr X is complete means :Def14: :: CLOPBAN1:def 14
for seq being sequence of X st seq is CCauchy holds
seq is convergent ;

end;

:: deftheorem Def14 defines complete CLOPBAN1:def 14 :

registration end;

definition

mode ComplexBanachSpace is complete ComplexNormSpace;

end;

Lm2: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e

proof end;

theorem Th45: :: CLOPBAN1:45

for X being ComplexNormSpace
for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )

proof end;

theorem Th46: :: CLOPBAN1:46

for X, Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is CCauchy holds
seq is convergent

proof end;

theorem Th47: :: CLOPBAN1:47

for X being ComplexNormSpace
for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace

proof end;

registration

let X be ComplexNormSpace;
let Y be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty complete ;
coherence by Th47;

end;