for seq1, seq2, seq3 being Complex_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th14;