( the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & ( for x being set holds
( x is VECTOR of Linear_Space_of_ComplexSequences iff x is Complex_Sequence ) ) & ( for u being VECTOR of Linear_Space_of_ComplexSequences holds u = seq_id u ) & ( for u, v being VECTOR of Linear_Space_of_ComplexSequences holds u + v = (seq_id u) + (seq_id v) ) & ( for z being Complex
for u being VECTOR of Linear_Space_of_ComplexSequences holds z * u = z (#) (seq_id u) ) ) by FUNCT_2:8, FUNCT_2:66, Th2, Th3;