environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CSSPACE, RSSPACE, SERIES_1, TARSKI, XCMPLX_0, COMSEQ_1, SEQ_1, SEQ_2, FUNCT_1, COMPLEX1, ARYTM_1, ORDINAL2, FUNCOP_1, ARYTM_3, XBOOLE_0, RLSUB_1, RLVECT_1, CARD_1, XXREAL_0, RELAT_1, VALUED_1, CLVECT_1, ALGSTR_0, CARD_3, BINOP_1, ZFMISC_1, STRUCT_0, SUPINF_2, NORMSP_1, REALSET1, PRE_TOPC, METRIC_1, REAL_1, NAT_1, RSSPACE3, XXREAL_2, CSSPACE3, NORMSP_0, RELAT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0, COMPLEX1, NAT_1, STRUCT_0, ALGSTR_0, RELAT_1, BINOP_1, REALSET1, DOMAIN_1, PARTFUN1, FUNCT_1, XXREAL_0, FUNCT_2, FUNCOP_1, PRE_TOPC, RLVECT_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, NORMSP_0, CLVECT_1, CSSPACE;
definitions NORMSP_0;
theorems RELAT_1, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SERIES_1, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, CSSPACE, CLVECT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, COMPLEX1, TARSKI, XBOOLE_0, RSSPACE2, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XCMPLX_0, XREAL_0, CSSPACE2, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, COMSEQ_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, COMSEQ_2, REALSET1, STRUCT_0, CLVECT_1, CSSPACE, VALUED_1, VALUED_0, XCMPLX_0, SEQ_2;
constructors HIDDEN, BINOP_1, FUNCOP_1, REAL_1, COMSEQ_2, COMSEQ_3, REALSET1, CSSPACE, SEQ_2, RELSET_1, CFUNCDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0, CSSPACE, CFUNCDOM;
expansions NORMSP_0;
Lm1:
CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is Subspace of Linear_Space_of_ComplexSequences
by CSSPACE:11;
registration
coherence
( CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital )
by CSSPACE:11;
end;
Lm2:
CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is ComplexLinearSpace
;
Lm3:
for c being Complex
for seq being Complex_Sequence
for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )