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