:: CSSPACE4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for rseq being Real_Sequence
for K being real number st ( for n being Nat holds rseq . n <= K ) holds
sup (rng rseq) <= K
proof end;

Lm2: for rseq being Real_Sequence st rseq is bounded holds
for n being Nat holds rseq . n <= sup (rng rseq)
proof end;

definition
func the_set_of_BoundedComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE4:def 1
for x being set holds
( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) );
existence
ex b1 being Subset of Linear_Space_of_ComplexSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_ComplexSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_set_of_BoundedComplexSequences CSSPACE4:def 1 :
for b1 being Subset of Linear_Space_of_ComplexSequences holds
( b1 = the_set_of_BoundedComplexSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) );

Lm3: for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
proof end;

Lm4: for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded
proof end;

registration
cluster the_set_of_BoundedComplexSequences -> non empty ;
coherence
not the_set_of_BoundedComplexSequences is empty
proof end;
cluster the_set_of_BoundedComplexSequences -> lineary-closed ;
coherence
the_set_of_BoundedComplexSequences is lineary-closed
proof end;
end;

Lm5: CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Subspace of Linear_Space_of_ComplexSequences
by CSSPACE:13;

registration
cluster CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence
( CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is ComplexLinearSpace-like ) by CSSPACE:13;
end;

Lm6: ( CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is ComplexLinearSpace-like )
;

Lm7: ex NORM being Function of the_set_of_BoundedComplexSequences , REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
NORM . x = sup (rng |.(seq_id x).|)
proof end;

definition
func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences , REAL means :Def2: :: CSSPACE4:def 2
for x being set st x in the_set_of_BoundedComplexSequences holds
it . x = sup (rng |.(seq_id x).|);
existence
ex b1 being Function of the_set_of_BoundedComplexSequences , REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
b1 . x = sup (rng |.(seq_id x).|) by Lm7;
uniqueness
for b1, b2 being Function of the_set_of_BoundedComplexSequences , REAL st ( for x being set st x in the_set_of_BoundedComplexSequences holds
b1 . x = sup (rng |.(seq_id x).|) ) & ( for x being set st x in the_set_of_BoundedComplexSequences holds
b2 . x = sup (rng |.(seq_id x).|) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def 2 :
for b1 being Function of the_set_of_BoundedComplexSequences , REAL holds
( b1 = Complex_linfty_norm iff for x being set st x in the_set_of_BoundedComplexSequences holds
b1 . x = sup (rng |.(seq_id x).|) );

Lm8: for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds
( seq is bounded & sup (rng |.seq.|) = 0 )
proof end;

Lm9: for seq being Complex_Sequence st seq is bounded holds
|.seq.| is bounded
proof end;

Lm10: for seq being Complex_Sequence st |.seq.| is bounded holds
seq is bounded
proof end;

Lm11: for seq being Complex_Sequence st seq is bounded & sup (rng |.seq.|) = 0 holds
for n being Nat holds seq . n = 0c
proof end;

theorem :: CSSPACE4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CSSPACE4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence holds
( ( seq is bounded & sup (rng |.seq.|) = 0 ) iff for n being Nat holds seq . n = 0c ) by Lm8, Lm11;

registration
cluster CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence
( CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is Abelian & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is add-associative & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is right_zeroed & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is right_complementable & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is ComplexLinearSpace-like ) by Lm6, CSSPACE3:4;
end;

definition
func Complex_linfty_Space -> non empty CNORMSTR equals :: CSSPACE4:def 3
 CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #);
coherence
CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is non empty CNORMSTR ;
end;

:: deftheorem defines Complex_linfty_Space CSSPACE4:def 3 :
Complex_linfty_Space = CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #);

theorem Th3: :: CSSPACE4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds
( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = sup (rng |.(seq_id v).|) ) )
proof end;

theorem Th4: :: CSSPACE4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Point of Complex_linfty_Space
for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| )
proof end;

registration
cluster Complex_linfty_Space -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like ;
coherence
( Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is ComplexLinearSpace-like & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable ) by Th4, CLVECT_1:def 10;
end;

Lm12: for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
proof end;

theorem Th5: :: CSSPACE4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for vseq being sequence of Complex_linfty_Space st vseq is CCauchy holds
vseq is convergent
proof end;

theorem :: CSSPACE4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Complex_linfty_Space is ComplexBanachSpace by Th5, CLOPBAN1:def 14;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
let IT be Function of X,the carrier of Y;
attr IT is bounded means :Def4: :: CSSPACE4:def 4
 ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) );
end;

:: deftheorem Def4 defines bounded CSSPACE4:def 4 :
for X being non empty set
for Y being ComplexNormSpace
for IT being Function of X,the carrier of Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ) );

theorem Th7: :: CSSPACE4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f being Function of X,the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
proof end;

registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster bounded Relation of X,the carrier of Y;
existence
ex b1 being Function of X,the carrier of Y st b1 is bounded
proof end;
end;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
func ComplexBoundedFunctions X,Y -> Subset of (ComplexVectSpace X,Y) means :Def5: :: CSSPACE4:def 5
for x being set holds
( x in it iff x is bounded Function of X,the carrier of Y );
existence
ex b1 being Subset of (ComplexVectSpace X,Y) st
for x being set holds
( x in b1 iff x is bounded Function of X,the carrier of Y )
proof end;
uniqueness
for b1, b2 being Subset of (ComplexVectSpace X,Y) st ( for x being set holds
( x in b1 iff x is bounded Function of X,the carrier of Y ) ) & ( for x being set holds
( x in b2 iff x is bounded Function of X,the carrier of Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def 5 :
for X being non empty set
for Y being ComplexNormSpace
for b3 being Subset of (ComplexVectSpace X,Y) holds
( b3 = ComplexBoundedFunctions X,Y iff for x being set holds
( x in b3 iff x is bounded Function of X,the carrier of Y ) );

registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster ComplexBoundedFunctions X,Y -> non empty ;
coherence
not ComplexBoundedFunctions X,Y is empty
proof end;
end;

theorem Th8: :: CSSPACE4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace holds ComplexBoundedFunctions X,Y is lineary-closed
proof end;

theorem Th9: :: CSSPACE4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace holds CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is Subspace of ComplexVectSpace X,Y
proof end;

registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence
( CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is Abelian & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is add-associative & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is right_zeroed & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is right_complementable & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is ComplexLinearSpace-like ) by Th9;
end;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
func C_VectorSpace_of_BoundedFunctions X,Y -> ComplexLinearSpace equals :: CSSPACE4:def 6
 CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #);
coherence
CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is ComplexLinearSpace ;
end;

:: deftheorem defines C_VectorSpace_of_BoundedFunctions CSSPACE4:def 6 :
for X being non empty set
for Y being ComplexNormSpace holds C_VectorSpace_of_BoundedFunctions X,Y = CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #);

registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster C_VectorSpace_of_BoundedFunctions X,Y -> strict ;
coherence
C_VectorSpace_of_BoundedFunctions X,Y is strict ;
end;

theorem :: CSSPACE4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th11: :: CSSPACE4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being VECTOR of (C_VectorSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )
proof end;

theorem Th12: :: CSSPACE4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions X,Y)
for f', h' being bounded Function of X,the carrier of Y st f' = f & h' = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h' . x = c * (f' . x) )
proof end;

theorem Th13: :: CSSPACE4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions X,Y) = X --> (0. Y)
proof end;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
let f be set ;
assume A1: f in ComplexBoundedFunctions X,Y ;
func modetrans f,X,Y -> bounded Function of X,the carrier of Y equals :Def7: :: CSSPACE4:def 7
f;
coherence
f is bounded Function of X,the carrier of Y by A1, Def5;
end;

:: deftheorem Def7 defines modetrans CSSPACE4:def 7 :
for X being non empty set
for Y being ComplexNormSpace
for f being set st f in ComplexBoundedFunctions X,Y holds
modetrans f,X,Y = f;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
let u be Function of X,the carrier of Y;
func PreNorms u -> non empty Subset of REAL equals :: CSSPACE4:def 8
{ ||.(u . t).|| where t is Element of X : verum } ;
coherence
{ ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL
proof end;
end;

:: deftheorem defines PreNorms CSSPACE4:def 8 :
for X being non empty set
for Y being ComplexNormSpace
for u being Function of X,the carrier of Y holds PreNorms u = { ||.(u . t).|| where t is Element of X : verum } ;

theorem Th14: :: CSSPACE4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for g being bounded Function of X,the carrier of Y holds
( not PreNorms g is empty & PreNorms g is bounded_above )
proof end;

theorem :: CSSPACE4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for g being Function of X,the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
proof end;

theorem Th16: :: CSSPACE4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace ex NORM being Function of ComplexBoundedFunctions X,Y, REAL st
for f being set st f in ComplexBoundedFunctions X,Y holds
NORM . f = sup (PreNorms (modetrans f,X,Y))
proof end;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
func ComplexBoundedFunctionsNorm X,Y -> Function of ComplexBoundedFunctions X,Y, REAL means :Def9: :: CSSPACE4:def 9
for x being set st x in ComplexBoundedFunctions X,Y holds
it . x = sup (PreNorms (modetrans x,X,Y));
existence
ex b1 being Function of ComplexBoundedFunctions X,Y, REAL st
for x being set st x in ComplexBoundedFunctions X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y)) by Th16;
uniqueness
for b1, b2 being Function of ComplexBoundedFunctions X,Y, REAL st ( for x being set st x in ComplexBoundedFunctions X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in ComplexBoundedFunctions X,Y holds
b2 . x = sup (PreNorms (modetrans x,X,Y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def 9 :
for X being non empty set
for Y being ComplexNormSpace
for b3 being Function of ComplexBoundedFunctions X,Y, REAL holds
( b3 = ComplexBoundedFunctionsNorm X,Y iff for x being set st x in ComplexBoundedFunctions X,Y holds
b3 . x = sup (PreNorms (modetrans x,X,Y)) );

theorem Th17: :: CSSPACE4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f being bounded Function of X,the carrier of Y holds modetrans f,X,Y = f
proof end;

theorem Th18: :: CSSPACE4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f being bounded Function of X,the carrier of Y holds (ComplexBoundedFunctionsNorm X,Y) . f = sup (PreNorms f)
proof end;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
func C_NormSpace_of_BoundedFunctions X,Y -> non empty CNORMSTR equals :: CSSPACE4:def 10
 CNORMSTR(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(ComplexBoundedFunctionsNorm X,Y) #);
coherence
CNORMSTR(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(ComplexBoundedFunctionsNorm X,Y) #) is non empty CNORMSTR ;
end;

:: deftheorem defines C_NormSpace_of_BoundedFunctions CSSPACE4:def 10 :
for X being non empty set
for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions X,Y = CNORMSTR(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(ComplexBoundedFunctionsNorm X,Y) #);

theorem Th19: :: CSSPACE4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions X,Y)
proof end;

theorem Th20: :: CSSPACE4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions X,Y)
for g being bounded Function of X,the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
proof end;

theorem :: CSSPACE4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions X,Y) holds 0 <= ||.f.||
proof end;

theorem Th22: :: CSSPACE4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions X,Y) st f = 0. (C_NormSpace_of_BoundedFunctions X,Y) holds
0 = ||.f.||
proof end;

theorem Th23: :: CSSPACE4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )
proof end;

theorem Th24: :: CSSPACE4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f, h being Point of (C_NormSpace_of_BoundedFunctions X,Y)
for f', h' being bounded Function of X,the carrier of Y st f' = f & h' = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h' . x = c * (f' . x) )
proof end;

theorem Th25: :: CSSPACE4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedFunctions X,Y)
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions X,Y) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions X,Y) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof end;

theorem Th26: :: CSSPACE4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions X,Y is ComplexNormSpace-like
proof end;

theorem Th27: :: CSSPACE4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions X,Y is ComplexNormSpace
proof end;

registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster C_NormSpace_of_BoundedFunctions X,Y -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like ;
coherence
( C_NormSpace_of_BoundedFunctions X,Y is ComplexNormSpace-like & C_NormSpace_of_BoundedFunctions X,Y is ComplexLinearSpace-like & C_NormSpace_of_BoundedFunctions X,Y is Abelian & C_NormSpace_of_BoundedFunctions X,Y is add-associative & C_NormSpace_of_BoundedFunctions X,Y is right_zeroed & C_NormSpace_of_BoundedFunctions X,Y is right_complementable ) by Th27;
end;

theorem Th28: :: CSSPACE4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f - g iff for x being Element of X holds h' . x = (f' . x) - (g' . x) )
proof end;

Lm13: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e
proof end;

theorem Th29: :: CSSPACE4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedFunctions X,Y) st seq is CCauchy holds
seq is convergent
proof end;

theorem Th30: :: CSSPACE4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions X,Y is ComplexBanachSpace
proof end;

registration
let X be non empty set ;
let Y be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedFunctions X,Y -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like complete ;
coherence
C_NormSpace_of_BoundedFunctions X,Y is complete by Th30;
end;

theorem :: CSSPACE4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded by Lm3;

theorem :: CSSPACE4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded by Lm4;

theorem :: CSSPACE4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence holds
( seq is bounded iff |.seq.| is bounded ) by Lm9, Lm10;

theorem :: CSSPACE4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) by Lm12;