let X be RealUnitarySpace; :: thesis:
let seq1, seq2 be sequence of X; :: thesis:
assume that
A1: seq1 is bounded and
A2: seq1 is_compared_to seq2 ; :: thesis:
consider m1 being Nat such that
A3: for n being Nat st n >= m1 holds
dist ((seq1 . n),(seq2 . n)) < 1 by A2;
consider p being Real such that
A4: p > 0 and
A5: for n being Nat holds ||.(seq1 . n).|| <= p by A1;
A6: ex M being Real st
( M > 0 & ( for n being Nat st n >= m1 holds
||.(seq2 . n).|| < M ) )

take M = p + 1; :: thesis:

let n be Nat; :: thesis:
assume n >= m1 ; :: thesis:
then dist ((seq1 . n),(seq2 . n)) < 1 by A3;
then A7: ||.((seq2 . n) - (seq1 . n)).|| < 1 by BHSP_1:def 5;
||.(seq2 . n).|| - ||.(seq1 . n).|| <= ||.((seq2 . n) - (seq1 . n)).|| by BHSP_1:32;
then ||.(seq2 . n).|| - ||.(seq1 . n).|| < 1 by A7, XXREAL_0:2;
then A8: ||.(seq2 . n).|| < ||.(seq1 . n).|| + 1 by XREAL_1:19;
||.(seq1 . n).|| <= p by A5;
then ||.(seq1 . n).|| + 1 <= p + 1 by XREAL_1:6;
hence ||.(seq2 . n).|| < M by A8, XXREAL_0:2; :: thesis:

end;

hence ( M > 0 & ( for n being Nat st n >= m1 holds
||.(seq2 . n).|| < M ) ) by A4; :: thesis:

end;

consider M2 being Real such that
A9: M2 > 0 and
A10: for n being Nat st n <= m1 holds
||.(seq2 . n).|| < M2 by Th8;
consider M1 being Real such that
A11: M1 > 0 and
A12: for n being Nat st n >= m1 holds
||.(seq2 . n).|| < M1 by A6;
take M = M1 + M2; :: thesis:
thus M > 0 by A11, A9; :: thesis:
let n be Nat; :: thesis:
A13: M > 0 + M2 by A11, XREAL_1:8;

end;

end;

hence ||.(seq2 . n).|| <= M by A14; :: thesis:

end;