for v, w being VECTOR of Linear_Space_of_ComplexSequences holds v + w = (seq_id v) + (seq_id w)