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