let X be RealUnitarySpace; :: 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

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

now

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

end;

hence seq is bounded by A4, Def3; :: thesis: verum

end;

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

proof

assume x <> H₁(X) ; :: thesis: seq is bounded
then A5: ( ||.x.|| >= 0 & ||.x.|| <> 0 ) by BHSP_1:32, BHSP_1:34;
consider M being real number such that
A6: ||.x.|| < M by XREAL_1:3;
reconsider M = M as Real by XREAL_0:def 1;
for n being Element of NAT holds ||.(seq . n).|| <= M by A1, A6;
hence seq is bounded by A5, A6, Def3; :: thesis: verum

end;

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