for r being Real
for v being VECTOR of Linear_Space_of_RealSequences holds r * v = r (#) (seq_id v)