environ
vocabularies HIDDEN, NUMBERS, SEQ_1, SUBSET_1, FUNCT_1, XXREAL_0, ORDINAL2, RELAT_1, XXREAL_2, CSSPACE, RSSPACE, TARSKI, COMSEQ_1, ARYTM_3, REAL_1, CARD_1, COMPLEX1, XCMPLX_0, VALUED_1, XBOOLE_0, RLSUB_1, RLVECT_1, CLVECT_1, ALGSTR_0, SEQ_4, STRUCT_0, SUPINF_2, ARYTM_1, NORMSP_1, ZFMISC_1, REALSET1, PRE_TOPC, MEMBER_1, NAT_1, RSSPACE3, SEQ_2, CLOPBAN1, FUNCOP_1, FUNCT_2, LOPBAN_1, REWRITE1, CSSPACE4, NORMSP_0, METRIC_1, RELAT_2, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, PRE_TOPC, DOMAIN_1, RELAT_1, FUNCOP_1, REALSET1, XXREAL_0, XREAL_0, XXREAL_2, XCMPLX_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, INTEGRA2, RLVECT_1, VALUED_1, COMSEQ_1, COMSEQ_2, NORMSP_0, NORMSP_1, SEQ_1, SEQ_2, CLVECT_1, SEQ_4, PARTFUN1, CSSPACE, CSSPACE3, CLOPBAN1;
definitions TARSKI, XBOOLE_0, NORMSP_0, XXREAL_2;
theorems RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, NAT_1, FUNCOP_1, SEQ_1, SEQ_2, SEQ_4, FUNCT_1, FUNCT_2, RLVECT_1, XREAL_0, XCMPLX_0, INTEGRA2, RSSPACE2, CSSPACE, COMSEQ_2, COMPLEX1, CLVECT_1, COMSEQ_1, CSSPACE3, COMSEQ_3, CLOPBAN1, XCMPLX_1, XREAL_1, XXREAL_0, LOPBAN_1, NORMSP_1, VALUED_1, MEASURE6, NORMSP_0, ORDINAL1;
schemes SEQ_1, FUNCT_2, XBOOLE_0, COMSEQ_1;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, STRUCT_0, CLVECT_1, CSSPACE3, VALUED_0, CSSPACE, VALUED_1, SEQ_2, SEQ_4, RFUNCT_1, NORMSP_0, RELSET_1, XCMPLX_0, NAT_1, SEQ_1;
constructors HIDDEN, REAL_1, COMPLEX1, COMSEQ_2, REALSET1, INTEGRA2, LOPBAN_1, CSSPACE3, CLOPBAN1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, SERIES_1, BINOP_1, SEQ_1, CFUNCDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities XBOOLE_0, REALSET1, CLOPBAN1, BINOP_1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0, CSSPACE, CFUNCDOM;
expansions TARSKI, XBOOLE_0, CLOPBAN1, NORMSP_0, XXREAL_2;
Lm1:
for rseq being Real_Sequence
for K being Real st ( for n being 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 Nat holds rseq . n <= upper_bound (rng rseq)
Lm3:
for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
reconsider jj = 1 as Real ;
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:11;
registration
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:11;
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:
for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds
( seq is bounded & upper_bound (rng |.seq.|) = 0 )
Lm8:
for seq being Complex_Sequence st seq is bounded holds
|.seq.| is bounded
Lm9:
for seq being Complex_Sequence st |.seq.| is bounded holds
seq is bounded
Lm10:
for seq being Complex_Sequence st seq is bounded & upper_bound (rng |.seq.|) = 0 holds
for n being Nat holds seq . n = 0c
registration
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:2;
end;
Lm11:
for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
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 Th7, CSSPACE:11;
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 Th7, CSSPACE:11;
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)))) #);
definition
let X be non
empty set ;
let Y be
ComplexNormSpace;
existence
ex b1 being Function of (ComplexBoundedFunctions (X,Y)),REAL st
for x being object st x in ComplexBoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
uniqueness
for b1, b2 being Function of (ComplexBoundedFunctions (X,Y)),REAL st ( for x being object st x in ComplexBoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in ComplexBoundedFunctions (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
end;
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)) #);
registration
let X be non
empty set ;
let Y be
ComplexNormSpace;
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 Th24;
end;
Lm12:
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