for z being Complex
for v being VECTOR of Linear_Space_of_ComplexSequences holds z * v = z (#) (seq_id v)