let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 - seq2 is bounded
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded ; :: thesis: seq1 - seq2 is bounded
A3: seq1 - seq2 = seq1 + (- seq2) by BHSP_1:71;
- seq2 is bounded by A2, Th19;
hence seq1 - seq2 is bounded by A1, A3, Th18; :: thesis: verum