A1: seq1 - seq2 = seq1 + (- seq2) by BHSP_1:49;
thus seq1 - seq2 is bounded by A1; :: thesis: verum