environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, RSSPACE, SERIES_1, TARSKI, REAL_1, SEQ_1, SEQ_2, FUNCT_1, COMPLEX1, ARYTM_1, ORDINAL2, ARYTM_3, CARD_1, XBOOLE_0, RLSUB_1, RLVECT_1, XXREAL_0, RELAT_1, VALUED_1, ALGSTR_0, CARD_3, BINOP_1, ZFMISC_1, NORMSP_1, STRUCT_0, SUPINF_2, REALSET1, PRE_TOPC, METRIC_1, NAT_1, XXREAL_2, RSSPACE3, NORMSP_0, RELAT_2, ASYMPT_1;
notations HIDDEN, TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, REALSET1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, FUNCT_1, FUNCT_2, RELAT_1, BINOP_1, FUNCOP_1, PRE_TOPC, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SERIES_1, PARTFUN1, FUNCSDOM, RSSPACE, XXREAL_0;
definitions NORMSP_0;
theorems XBOOLE_0, RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SERIES_1, COMSEQ_3, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, RLSUB_1, NORMSP_1, XREAL_0, SEQ_4, RSSPACE, RSSPACE2, COMPLEX1, XREAL_1, XXREAL_0, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, XBOOLE_0;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, NORMSP_1, RSSPACE, VALUED_1, FUNCT_2, SEQ_4, VALUED_0, SEQ_1, SEQ_2, FUNCSDOM;
constructors HIDDEN, PARTFUN1, BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQ_2, SERIES_1, REALSET1, RLSUB_1, RSSPACE, VALUED_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, FUNCSDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1, REALSET1, RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0, RSSPACE, SEQ_1, FUNCSDOM;
expansions NORMSP_0;
Lm1:
RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:11;
registration
coherence
( RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital )
by RSSPACE:11;
end;
Lm2:
RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is RealLinearSpace
;
Lm3:
for c being Real
for seq, 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) )