theorem Th9: :: NDIFF_1:9

for S being RealNormSpace
for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)