begin
Lm1:
for rseq being Real_Sequence
for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
Lm2:
for rseq being Real_Sequence st rseq is bounded holds
for n being Element of NAT holds rseq . n <= upper_bound (rng rseq)
:: 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
Lm4:
for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded
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 ) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
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 vector-distributive & 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 scalar-distributive & 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 scalar-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 scalar-unital )
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 vector-distributive & 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 scalar-distributive & 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 scalar-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 scalar-unital )
;
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 = upper_bound (rng |.(seq_id x).|)
:: 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 = upper_bound (rng |.(seq_id x).|) );
Lm8:
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
( seq is bounded & upper_bound (rng |.seq.|) = 0 )
Lm9:
for seq being Complex_Sequence st seq is bounded holds
|.seq.| is bounded
Lm10:
for seq being Complex_Sequence st |.seq.| is bounded holds
seq is bounded
Lm11:
for seq being Complex_Sequence st seq is bounded & upper_bound (rng |.seq.|) = 0 holds
for n being Element of NAT holds seq . n = 0c
theorem
canceled;
theorem
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 #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
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 vector-distributive & 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 scalar-distributive & 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 scalar-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 scalar-unital )
by Lm6, CSSPACE3:4;
end;
definition
func Complex_linfty_Space -> non
empty CNORMSTR equals
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:
theorem Th4:
Lm12:
for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
theorem Th5:
theorem
begin
:: 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:
:: 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 ) );
theorem Th8:
theorem
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 by Th8, CSSPACE:13;
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)) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
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 vector-distributive & 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 scalar-distributive & 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 scalar-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 scalar-unital )
by Th8, CSSPACE:13;
end;
definition
let X be non
empty set ;
let Y be
ComplexNormSpace;
func C_VectorSpace_of_BoundedFunctions X,
Y -> ComplexLinearSpace equals
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)) #);
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
:: 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;
:: 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:
theorem
theorem Th16:
definition
let X be non
empty set ;
let Y be
ComplexNormSpace;
func ComplexBoundedFunctionsNorm X,
Y -> Function of
(ComplexBoundedFunctions X,Y),
REAL means :
Def9:
for
x being
set st
x in ComplexBoundedFunctions X,
Y holds
it . x = upper_bound (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 = upper_bound (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 = upper_bound (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in ComplexBoundedFunctions X,Y holds
b2 . x = upper_bound (PreNorms (modetrans x,X,Y)) ) holds
b1 = b2
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 = upper_bound (PreNorms (modetrans x,X,Y)) );
theorem Th17:
theorem Th18:
definition
let X be non
empty set ;
let Y be
ComplexNormSpace;
func C_NormSpace_of_BoundedFunctions X,
Y -> non
empty CNORMSTR equals
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:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
registration
let X be non
empty set ;
let Y be
ComplexNormSpace;
cluster C_NormSpace_of_BoundedFunctions X,
Y -> non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
( C_NormSpace_of_BoundedFunctions X,Y is reflexive & C_NormSpace_of_BoundedFunctions X,Y is discerning & C_NormSpace_of_BoundedFunctions X,Y is ComplexNormSpace-like & C_NormSpace_of_BoundedFunctions X,Y is vector-distributive & C_NormSpace_of_BoundedFunctions X,Y is scalar-distributive & C_NormSpace_of_BoundedFunctions X,Y is scalar-associative & C_NormSpace_of_BoundedFunctions X,Y is scalar-unital & 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:
Lm13:
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
theorem Th29:
theorem Th30:
begin
theorem
theorem
theorem
theorem