let X be ComplexUnitarySpace; :: 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 p being Real such that
A3: p > 0 and
A4: for n being Element of NAT holds ||.(seq1 . n).|| <= p by A1, Def10;
consider m1 being Element of NAT such that
A5: for n being Element of NAT st n >= m1 holds
dist (seq1 . n),(seq2 . n) < 1 by A2, Def9;
A6: p + 1 > 0 + 0 by A3;
A7: ex M being Real st
( M > 0 & ( for n being Element of NAT st n >= m1 holds
||.(seq2 . n).|| < M ) )

proof

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

now

let n be Element of NAT ; :: thesis: ( n >= m1 implies ||.(seq2 . n).|| < M )
assume n >= m1 ; :: thesis: ||.(seq2 . n).|| < M
then dist (seq1 . n),(seq2 . n) < 1 by A5;
then A8: ||.((seq2 . n) - (seq1 . n)).|| < 1 by CSSPACE:def 16;
||.(seq2 . n).|| - ||.(seq1 . n).|| <= ||.((seq2 . n) - (seq1 . n)).|| by CSSPACE:50;
then ||.(seq2 . n).|| - ||.(seq1 . n).|| < 1 by A8, XXREAL_0:2;
then A9: ||.(seq2 . n).|| < ||.(seq1 . n).|| + 1 by XREAL_1:21;
||.(seq1 . n).|| <= p by A4;
then ||.(seq1 . n).|| + 1 <= p + 1 by XREAL_1:8;
hence ||.(seq2 . n).|| < M by A9, XXREAL_0:2; :: thesis: verum

end;

hence ( M > 0 & ( for n being Element of NAT st n >= m1 holds
||.(seq2 . n).|| < M ) ) by A6; :: thesis: verum

end;

now

consider M1 being Real such that
A10: M1 > 0 and
A11: for n being Element of NAT st n >= m1 holds
||.(seq2 . n).|| < M1 by A7;
consider M2 being Real such that
A12: M2 > 0 and
A13: for n being Element of NAT st n <= m1 holds
||.(seq2 . n).|| < M2 by Th79;
take M = M1 + M2; :: thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq2 . n).|| <= M ) )
M > 0 + 0 by A10, A12;
hence M > 0 ; :: thesis: for n being Element of NAT holds ||.(seq2 . n).|| <= M
A14: M > M1 + 0 by A12, XREAL_1:10;
A15: M > 0 + M2 by A10, XREAL_1:10;
let n be Element of NAT ; :: thesis: ||.(seq2 . n).|| <= M

A16: now

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

end;

now

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

end;

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

end;

hence seq2 is bounded by Def10; :: thesis: verum