let seq1, seq2, seq3 be Real_Sequence; :: thesis: (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
thus (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) + ((- seq2) (#) seq3) by Th15
.= (seq1 (#) seq3) - (seq2 (#) seq3) by Th18 ; :: thesis: verum