let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is convergent holds
seq is bounded
let seq be sequence of X; :: thesis: ( seq is convergent implies seq is bounded )
assume seq is convergent ; :: thesis: seq is bounded
then consider g being Point of X such that
A1: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r by Th9;
consider m1 being Element of NAT such that
A2: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < 1 by A1;

A3: now

take p = ||.g.|| + 1; :: thesis: ( p > 0 & ( for n being Element of NAT st n >= m1 holds
||.(seq . n).|| < p ) )
0 + 0 < p by CSSPACE:46, XREAL_1:10;
hence p > 0 ; :: thesis: for n being Element of NAT st n >= m1 holds
||.(seq . n).|| < p
let n be Element of NAT ; :: thesis: ( n >= m1 implies ||.(seq . n).|| < p )
assume n >= m1 ; :: thesis: ||.(seq . n).|| < p
then A4: ||.((seq . n) - g).|| < 1 by A2;
||.(seq . n).|| - ||.g.|| <= ||.((seq . n) - g).|| by CSSPACE:50;
then ||.(seq . n).|| - ||.g.|| < 1 by A4, XXREAL_0:2;
hence ||.(seq . n).|| < p by XREAL_1:21; :: thesis: verum

end;

now

consider M1 being Real such that
A5: M1 > 0 and
A6: for n being Element of NAT st n >= m1 holds
||.(seq . n).|| < M1 by A3;
consider M2 being Real such that
A7: M2 > 0 and
A8: for n being Element of NAT st n <= m1 holds
||.(seq . n).|| < M2 by Th79;
take M = M1 + M2; :: thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) )
M > 0 + 0 by A5, A7;
hence M > 0 ; :: thesis: for n being Element of NAT holds ||.(seq . n).|| <= M
A9: M > M1 + 0 by A7, XREAL_1:10;
A10: M > 0 + M2 by A5, XREAL_1:10;
let n be Element of NAT ; :: thesis: ||.(seq . n).|| <= M

A11: now

assume n >= m1 ; :: thesis: ||.(seq . n).|| <= M
then ||.(seq . n).|| < M1 by A6;
hence ||.(seq . n).|| <= M by A9, XXREAL_0:2; :: thesis: verum

end;

now

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

end;

hence ||.(seq . n).|| <= M by A11; :: thesis: verum

end;

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