let seq1, seq2, seq3 be Complex_Sequence; :: thesis: (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
thus (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) + ((- seq2) (#) seq3) by Th9
.= (seq1 (#) seq3) + (((- 1r) (#) seq2) (#) seq3)
.= (seq1 (#) seq3) + ((- 1r) (#) (seq2 (#) seq3)) by Th12
.= (seq1 (#) seq3) - (seq2 (#) seq3) ; :: thesis: verum