theorem Th12: :: NDIFF_1:12

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