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