let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is constant holds
seq is bounded
let seq be sequence of X; :: thesis: ( seq is constant implies seq is bounded )
assume seq is constant ; :: thesis: seq is bounded
then consider x being Point of X such that
A1: for n being Nat holds seq . n = x by VALUED_0:def 18;
A2: ( x = H₂(X) implies seq is bounded )

proof

consider M being real number such that
A3: M > 0 by XREAL_1:1;
reconsider M = M as Real by XREAL_0:def 1;
assume A4: x = H₂(X) ; :: thesis: seq is bounded

now

let n be Element of NAT ; :: thesis: ||.(seq . n).|| <= M
seq . n = H₂(X) by A1, A4;
hence ||.(seq . n).|| <= M by A3, CSSPACE:42; :: thesis: verum

end;

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

end;

( x <> H₂(X) implies seq is bounded )

proof

assume x <> H₂(X) ; :: thesis: seq is bounded
consider M being real number such that
A5: ||.x.|| < M by XREAL_1:1;
reconsider M = M as Real by XREAL_0:def 1;
( ||.x.|| >= 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ) by A1, A5, CSSPACE:44;
hence seq is bounded by A5, Def10; :: thesis: verum

end;

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