for r being Complex
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)