let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded )
assume that
A1: seq1 is bounded and
A2: seq1 is_compared_to seq2 ; :: thesis: seq2 is bounded
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 ) )

proof

take M = p + 1; :: thesis: ( M > 0 & ( for n being Nat st n >= m1 holds
||.(seq2 . n).|| < M ) )

now :: thesis: for n being Nat st n >= m1 holds
||.(seq2 . n).|| < M

let n be Nat; :: thesis: ( n >= m1 implies ||.(seq2 . n).|| < M )
assume n >= m1 ; :: thesis: ||.(seq2 . n).|| < M
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: verum

end;

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

end;

now :: thesis: ex M being set st
( M > 0 & ( for n being Nat holds ||.(seq2 . n).|| <= M ) )

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: ( M > 0 & ( for n being Nat holds ||.(seq2 . n).|| <= M ) )
thus M > 0 by A11, A9; :: thesis: for n being Nat holds ||.(seq2 . n).|| <= M
let n be Nat; :: thesis: ||.(seq2 . n).|| <= M
A13: M > 0 + M2 by A11, XREAL_1:8;

A14: now :: thesis: ( n <= m1 implies ||.(seq2 . n).|| <= M )

assume n <= m1 ; :: thesis: ||.(seq2 . n).|| <= M
then ||.(seq2 . n).|| < M2 by A10;
hence ||.(seq2 . n).|| <= M by A13, XXREAL_0:2; :: thesis: verum

end;

A15: M > M1 + 0 by A9, XREAL_1:8;

now :: thesis: ( n >= m1 implies ||.(seq2 . n).|| <= M )

assume n >= m1 ; :: thesis: ||.(seq2 . n).|| <= M
then ||.(seq2 . n).|| < M1 by A12;
hence ||.(seq2 . n).|| <= M by A15, XXREAL_0:2; :: thesis: verum

end;

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

end;

hence seq2 is bounded ; :: thesis: verum