begin
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
;
begin
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 Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )