let X be ComplexUnitarySpace; :: 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 CSSPACE:64;
- seq2 is bounded by A2, Th75;
hence seq1 - seq2 is bounded by A1, A3, Th74; :: thesis: verum