theorem :: RSSPACE:2

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