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